importCTLimportModelimportMCimportExtra

Here is a model for the circuit that was used in the Model Checking lectures.

The state `S` consists of three bits: the input `dreq` and the output of the
two latches `(q0,dack)`.

The atomic formulas `A` are represented as functions from the state `S` to Bool.

typeS=(Bool,(Bool,Bool))typeA=S->Boolm::ModelASm=Model{next=next,atom=id}wherenext(dreq,(q0,dack))=[(False,s'),(True,s')]wheres'=(q0',dack')q0'=dreqdack'=dreq&&(q0||notq0&&dack)s0::Ss0=(False,(False,False))

Some atomic formulas:

a0,a1,a2,a3,a4::Aa0s=s==s0a1(dreq,(q0,dack))=dreq&&q0&&dacka2(dreq,(q0,dack))=(dreq||q0)&&dacka3(dreq,(q0,dack))=notq0&&dacka4(dreq,(q0,dack))=dreqa5(dreq,(q0,dack))=dack

Some CTL formulas built from the above atomic formulas:

p1,p2,p3,p4::CTLAp1=EF(Atoma1)p2=EG(Atoma2)p3=Not(Atoma3)&EF(Atoma3)p4=ag(Not(Atoma4)==>ax(Not(Atoma5)))

Testing the Model Checker on the above formulas.

The `B` is just there to make the output more readable. It shows
states as e.g. `000` instead of `(False,(False,False))`.

test1=B(mcmp1)test2=B(mcmp2)test3=B(mcmp3)test4=B(mcmp4)

A main function to show the state transitions and run all test tests:

main=doputStrLn"State transitions in the model:"transitionsm)putStrLn"Results of model checking:"putStr"p1: ";test1putStr"p2: ";test2putStr"p3: ";test3putStr"p4: ";test4