// CONNECTORS -----------------------------------------------
// Classical operators
connector and     2 true  "_ & _" 3
connector not     1 false "~_"    5

// Modal operators
connector nec     1 false "[]_"   4

//isItSat connector :)
connector isItSat 1 false "isItSat[_]?" 4
//---------------------------------------------------------------------
//modelChecking isItSat
//---------------------------------------------------------------------
// TABLEAU RULES -------------------------------------------

// buildModel
rule buildModel
	if isNewNode node0
	do add node0  (constant p) 
	do newNode node2
	do link node0 node2 (R)
	do add node2 (not (constant p))
	do newNode node1
	do link node0 node1 (R)
	do add node1 (constant p)
	do newNode node3
	do link node1 node3 (R)
	do add node3 (not (constant p))
	do newNode node4
	do link node1 node4 (R)
	do add node4 (not (constant p))
end

//	        node0 [p]
//	         /         \
//	        /           \
//	node2[~p]   node1[p]
//	                    /          \
//	                  /              \
//	        node3[~p]       node4[~p]
//-----------------------------------------------------------

rule buildModel2
if isNewNode n0
do newNode n01
do link n0 n01 (R)
do newNode n02
do link n0 n02 (R)
do newNode n03
do link n0 n03 (R)
do newNode n011
do link n01 n011 (R)
do newNode n021
do link n02 n021 (R)
do newNode n022
do link n02 n022 (R)
do newNode n023
do link n02 n023 (R)
do newNode n031
do link n03 n031 (R)
do newNode n032
do link n03 n032 (R)
do newNode n0111
do link n011 n0111 (R)
do newNode n0221
do link n022 n0221 (R)
do add n0 constant p
do add n0 constant q
do add n01 constant p
do add n01 not constant q
do add n02 constant p
do add n02 constant q
do add n03 not constant p
do add n03 constant q
do add n011 not constant p
do add n011 not constant q
do add n021 not constant p
do add n021 constant q
do add n022 not constant p
do add n022 constant q
do add n023 not constant p
do add n023 not constant q
do add n031 constant p
do add n031 constant q
do add n032 not constant p
do add n032 constant q
do add n0111 constant p
do add n0111 constant q
do add n0221 not constant p
do add n0221 constant q
end

//-----------------------------------------------------------


//----------------------------------------------
//           Propagate Down
//----------------------------------------------
// prop down nec
rule propDownNec
if hasElement n0 isItSat nec variable A
if isLinked n0 n1 R
do add n1 isItSat variable A
end

rule propDownNotNec
if hasElement n0 isItSat not nec variable A
if isLinked n0 n1 R
do add n1 isItSat not variable A
end
//----------------------------------------------
// prop down and
rule propDownAnd
if hasElement n0 isItSat and variable A variable B
do add n0 isItSat variable A
do add n0 isItSat variable B
end

//-----------------------------------------------
// prop down not and
rule propDownNotAnd
if hasElement n0 isItSat not and variable A variable B
do add n0 isItSat not variable A
do add n0 isItSat not variable B
end

//-----------------------------------------------
// prop down not not
rule propDownNoNot
if hasElement n0 isItSat not not variable A
do add n0 isItSat variable A
end


//-----------------------------------------------
//      Resolve with litterals & at Leaf
//-----------------------------------------------

rule resolveWhenSat
if hasElement n0 isItSat variable A
if hasElement n0 variable A
do markExpressions n0 isItSat variable A "Yes it's Sat"
end

rule resolveWhenNotSat
if hasElement n0 isItSat variable A
if hasElement n0 not variable A
do markExpressions n0 isItSat variable A "No it isn't Sat"
end

rule resolveWithNot
if hasElement n0 isItSat not variable A
if hasElement n0 variable A
do markExpressions n0 isItSat not variable A "No it isn't Sat"
end
//-----------------------------------------------
// Resolve nec (at leaf)
rule propUpNecAtLeaf
if hasElement n0 isItSat nec variable A
if hasNoSuccessor n0 (R)
do markExpressions n0 isItSat nec variable A "Yes it's Sat"
end

//-----------------------------------------------
// Resolve not nec (at leaf)
rule propUpNotNecAtLeaf
if hasElement n0 isItSat not nec variable A
if hasNoSuccessor n0 (R)
do markExpressions n0 isItSat not nec variable A "No it isn't Sat"
end

//-----------------------------------------------

//-----------------------------------------------
//       Propagate Up with formulae 
//-----------------------------------------------
// prop up nec (with formulae)
rule propUpNecNotSat
if hasElement n0 isItSat nec variable A
if isLinked n0 n1 R
if isMarkedExpression n1 isItSat variable A "No it isn't Sat"
do unmarkExpressions n0 isItSat nec variable A "Yes it's Sat"
do markExpressions n0 isItSat nec variable A "No it isn't Sat"
end

rule propUpNecSat
if hasElement n0 isItSat nec variable A
if isLinked n0 n1 R
if isMarkedExpression n1 isItSat variable A "Yes it's Sat"
if isNotMarkedExpression n0 isItSat nec variable A "No it isn't Sat"
do markExpressions n0 isItSat nec variable A "Yes it's Sat"
end

rule propUpNotNecNotSat
if hasElement n0 isItSat not nec variable A
if isLinked n0 n1 R
if isMarkedExpression n1 isItSat not variable A "No it isn't Sat"
if isNotMarkedExpression n0 isItSat not nec variable A "Yes it's Sat"
do markExpressions n0 isItSat not nec variable A "No it isn't Sat"
end

rule propUpNotNecSat
if hasElement n0 isItSat not nec variable A
if isLinked n0 n1 R
if isMarkedExpression n1 isItSat not variable A "Yes it's Sat"
do unmarkExpressions n0 isItSat not nec variable A "No it isn't Sat"
do markExpressions n0 isItSat not nec variable A "Yes it's Sat"
end
//-------------------------------------------------
// prop up and (with formulae)
rule propUpAndLeft
if hasElement n0 isItSat and variable A variable B
if isMarkedExpression n0 isItSat variable A "No it isn't Sat"
if isMarkedExpression n0 isItSat variable B "Yes it's Sat"
do unmarkExpressions n0 isItSat and variable A variable B "Yes it's Sat" //precaution
do markExpressions n0 isItSat and variable A variable B "No it isn't Sat"
end

rule propUpAndRight
if hasElement n0 isItSat and variable A variable B
if isMarkedExpression n0 isItSat variable A "Yes it's Sat"
if isMarkedExpression n0 isItSat variable B "No it isn't Sat"
do unmarkExpressions n0 isItSat and variable A variable B "Yes it's Sat" //precaution
do markExpressions n0 isItSat and variable A variable B "No it isn't Sat"
end

rule propUpAndBothSat
if hasElement n0 isItSat and variable A variable B
if isMarkedExpression n0 isItSat variable A "Yes it's Sat"
if isMarkedExpression n0 isItSat variable B "Yes it's Sat"
do unmarkExpressions n0 isItSat and variable A variable B "No it isn't Sat" //precaution
do markExpressions n0 isItSat and variable A variable B "Yes it's Sat"
end

rule propUpAndBothNotSat
if hasElement n0 isItSat and variable A variable B
if isMarkedExpression n0 isItSat variable A "No it isn't Sat"
if isMarkedExpression n0 isItSat variable B "No it isn't Sat"
do unmarkExpressions n0 isItSat and variable A variable B "Yes it's Sat" //precaution
do markExpressions n0 isItSat and variable A variable B "No it isn't Sat"
end
//------------------------------------------------------
// prop up not and (with formulae)

rule propUpNotAndLeft
if hasElement n0 isItSat not and variable A variable B
if isMarkedExpression n0 isItSat not variable A "Yes it's Sat"
if isMarkedExpression n0 isItSat not variable B "No it isn't Sat"
do unmarkExpressions n0 isItSat not and variable A variable B "No it isn't Sat" //precaution
do markExpressions n0 isItSat not and variable A variable B "Yes it's Sat"
end

rule propUpNotAndRight
if hasElement n0 isItSat not and variable A variable B
if isMarkedExpression n0 isItSat not variable A "No it isn't Sat"
if isMarkedExpression n0 isItSat not variable B "Yes it's Sat"
do unmarkExpressions n0 isItSat not and variable A variable B "No it isn't Sat" //precaution
do markExpressions n0 isItSat not and variable A variable B "Yes it's Sat"
end

rule propUpNotAndBothSat
if hasElement n0 isItSat not and variable A variable B
if isMarkedExpression n0 isItSat not variable A "Yes it's Sat"
if isMarkedExpression n0 isItSat not variable B "Yes it's Sat"
do unmarkExpressions n0 isItSat not and variable A variable B "No it isn't Sat"  //precaution
do markExpressions n0 isItSat not and variable A variable B "Yes it's Sat"
end

rule propUpNotAndBothNotSat
if hasElement n0 isItSat not and variable A variable B
if isMarkedExpression n0 isItSat not variable A "No it isn't Sat"
if isMarkedExpression n0 isItSat not variable B "No it isn't Sat"
do unmarkExpressions n0 isItSat not and variable A variable B "Yes it's Sat"  //precaution
do markExpressions n0 isItSat not and variable A variable B "No it isn't Sat"
end
//--------------------------------------------------------
// prop up not not (with formulae)
rule propUpNoNotSat
if hasElement n0 isItSat not not variable A
if isMarkedExpression n0 isItSat variable A "Yes it's Sat"
do markExpressions n0 isItSat not not variable A "Yes it's Sat"
end

rule propUpNoNotNotSat
if hasElement n0 isItSat not not variable A
if isMarkedExpression n0 isItSat variable A "No it isn't Sat"
do markExpressions n0 isItSat not not variable A "No it isn't Sat"
end