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