# testmc.hs

Plain text version of testmc.hs

## 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
```