LoTREC Support for Model-Checking

LoTREC home page

Model Checking main page

Rules and strategy Definition

You can download the files moelchecking.cr et modelchecking.str.

The connectors definition:

// 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

The rules definition:

// 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]
//----------------------------------------------
 

//----------------------------------------------
// 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
 

The model-checking strategy:

// STRATEGIES -------------------------------------
strategy propagateDownFormulae
firstRule
propDownNec
propDownNotNec
propDownAnd
propDownNotAnd
propDownNoNot
end
end

strategy resolveWithLittAndAtLeaf
firstRule
resolveWhenSat
resolveWhenNotSat
resolveWithNot

propUpNecAtLeaf
propUpNotNecAtLeaf
end
end

strategy propagateUpFormulae
firstRule
propUpNecSat
propUpNecNotSat
propUpNotNecSat
propUpNotNecNotSat

propUpAndLeft
propUpAndRight
propUpAndBothSat
propUpAndBothNotSat

propUpNotAndLeft
propUpNotAndRight
propUpNotAndBothSat
propUpNotAndBothNotSat

propUpNoNotSat
propUpNoNotNotSat
end
end

//-------------------------------------------------
//Global strategy
strategy modelChecking
allRules
buildModel
repeat
propagateDownFormulae
end
repeat
resolveWithLittAndAtLeaf
end
repeat
propagateUpFormulae
end
end
end

Back to main page