{-+
Testing the simple model checker
--------------------------------
-}
import CTL
import Model
import MC
import Extra

{-+
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.
-}
type S = (Bool,(Bool,Bool))
type A = S->Bool

m :: Model A S
m = Model { next = next, atom = id }
  where
    next (dreq,(q0,dack)) = [(False,s'),(True,s')]
      where
        s' = (q0',dack')
        q0' = dreq
        dack' = dreq && (q0 || not q0 && dack)

s0 :: S
s0 = (False,(False,False))

{-+
Some atomic formulas:
-}
a0,a1,a2,a3,a4 :: A
a0 s = s==s0
a1 (dreq,(q0,dack)) = dreq && q0 && dack
a2 (dreq,(q0,dack)) = (dreq || q0) && dack
a3 (dreq,(q0,dack)) = not q0 && dack
a4 (dreq,(q0,dack)) = dreq
a5 (dreq,(q0,dack)) = dack
{-+
Some CTL formulas built from the above atomic formulas:
-}
p1,p2,p3,p4 :: CTL A
p1 = EF (Atom a1)
p2 = EG (Atom a2)
p3 = Not (Atom a3) & EF (Atom a3)
p4 = ag (Not (Atom a4) ==> ax (Not (Atom a5)))

{-+
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 (mc m p1)
test2 = B (mc m p2)
test3 = B (mc m p3)
test4 = B (mc m p4)

{-+
A main function to show the state transitions and run all test tests:
-}
main = do putStrLn "State transitions in the model:"
          print (transitions m)

          putStrLn "Results of model checking:"
          putStr "p1: "; print test1
          putStr "p2: "; print test2
          putStr "p3: "; print test3
          putStr "p4: "; print test4