The SmlMC Model Checker 
by Wouter Boekke

Listing One
open SmlMC_head

val with_timing = false
val model_check = false

datatype Component =
  Buffer of { cnt:int }
val buffer = ref(Buffer{cnt=0})
val components = #[ buffer ]
val (e1,e2) = (nop(),nop())
val get_b = fn ref(Buffer d) => d
val events = init_ev
[ ev e1
  ( fn() =>
    ( let val n = #cnt (get_b buffer)
      in
        if n < 3 then buffer := Buffer{cnt=n+1} else ()
      end;
      act e1
    )
  ),
  ev e2
  ( fn() =>
    ( let val n = #cnt (get_b buffer)
      in
        if n > 0 then buffer := Buffer{cnt=n-1} else ()
      end;
      act e2
    )
  )
]
val _ = ( act e1; act e2 )
val print_comp = fn
  Buffer{cnt=n} => pr.printq `buffer(^(pr.d n))`

Listing Two
start: buffer(0)
  sta: 0 - buffer(0) ev:2
  sta: 1 - buffer(0) ev:1
  tra: 0 1
  sta: 2 - buffer(1) ev:1
  tra: 0 2
  sta: 3 - buffer(2) ev:1
  tra: 2 3
  tra: 1 1
  sta: 4 - buffer(3) ev:1
  tra: 3 4
  tra: 4 4
5 states


Listing Three
structure dut = struct
local
  open SmlMC_head
in
val with_timing = true
val model_check = true
val _ = perm_max := 3
val (PRC,SEC,DNU,undef) = (4,3,2,1)
val (pr_1,pr_2,pr_3,dis) = (4,3,2,1)

type Ssm = { ql:int }

datatype Component =
  Clock of Ssm
| Ne of string * int * Ssm * Ssm * Ssm * Ssm
        (* id,q,in1,in2,out1,out2 *)
| Con of bool

structure ne = struct
  val get = fn ref(Ne t) => t | _ => err "Ne"
  fun set this f = this := Ne(f(get this))
  fun id   t = #1 (get t)
  fun q    t = #2 (get t)
  fun in1  t = #3 (get t)
  fun in2  t = #4 (get t)
  fun out1 t = #5 (get t)
  fun out2 t = #6 (get t)
end

datatype Var_Fix =
  Ne_vf of { var:Component ref, fix:{ prov:int Vector.vector, 
                                                    i3:Component ref } }
val get_con = fn ref(Con on) => on | _ => err "get_con"
val get_ck = fn ref(Clock d) => d | _ => err "get_ck"
val [ck,w1,w2,w3,w4,w11,w12,w13,w14,con] = List.tabulate(10,fn _ => nop())
val dummy = { ql=undef }
val clock = { ql=PRC }
val no_clock = ref(Clock dummy)
val okay = ref(Con true)
val ck1=ref(Clock clock)
val con1=ref(Con true)

fun init id = (id,0,dummy,dummy,dummy,dummy)
val (ne0,ne1,ne2,ne3) =
( Ne_vf{ var=ref(Ne(init "ne0")), 
                            fix={ prov= #[0,dis,pr_2,pr_1], i3=ck1 } },
  Ne_vf{ var=ref(Ne(init "ne1")), 
                            fix={ prov= #[0,pr_1,pr_2,dis], i3=no_clock } },
  Ne_vf{ var=ref(Ne(init "ne2")), 
                            fix={ prov= #[0,pr_1,pr_2,dis], i3=no_clock } },
  Ne_vf{ var=ref(Ne(init "ne3")), 
                            fix={ prov= #[0,pr_1,pr_2,dis], i3=no_clock } }
)
val components =
  let fun get (Ne_vf{ var=v, ...}) = v
  in #[ ck1,get ne0,get ne1,get ne2,get ne3,con1 ]
  end
val \ = fn(a,c) => Vector.sub(a,c)
infix 9 \
fun for(a,b,f) = if a>b then () else (f(a); for(a+1,b,f))

datatype Sig_flow = o1_i1 | o2_i2

fun ne_update (Ne_vf snd) (Ne_vf rcv) sig_flow con =
  let
  fun sel_alg({ql=ql1},{ql=ql2},{ql=ql3},q) =
    let
      val ql = #[undef,ql1,ql2,ql3]
      val q = ref q
      val prov = #prov(#fix rcv)
    in
      if prov\(!q) = dis orelse ql\(!q) <= DNU then q := 0 else ();
      for (1,3,fn p =>
        if prov\p <> dis andalso ql\p > DNU andalso
           ( ql\p > ql\(!q)
             orelse
             ql\p = ql\(!q) andalso prov\p > prov\(!q)
           )

        then q := p
        else ()
      );
      (ql\(!q),!q)
    end
  val (i1,i2) = if sig_flow = o1_i1
    then (if (get_con con) then ne.out1(#var snd) else dummy,ne.in2(#var rcv))
    else (ne.in1(#var rcv),if (get_con con) then ne.out2(#var snd) else dummy)
  val (ql_in,q) = sel_alg(i1,i2,get_ck(#i3(#fix rcv)),ne.q(#var rcv))
  val (ql_out,q) = (if ql_in < SEC then (SEC,0) else (ql_in,q))
  val (out1,out2) =
    case q of
        3 => ({ ql=ql_out }, { ql=ql_out })
      | 2 => ({ ql=DNU },    { ql=ql_out })
      | 1 => ({ ql=ql_out }, { ql=DNU })
      | 0 => ({ ql=ql_out }, { ql=ql_out })
      | _ => err "q"
  in
    ne.set (#var rcv) (fn(id,_,_,_,_,_)=>(id,q,i1,i2,out1,out2))
  end

fun evn(snd,rcv,sflow,act1,act2,on) =
  fn() =>
  ( ne_update snd rcv sflow on;
    act act1; act act2
  )
val events = init_ev
[ ev_choice ck [ fn() => (ck1 := Clock dummy; act ck),
                 fn() => (ck1 := Clock clock; act ck)
               ],
  ev w1  (evn(ne0,ne1,o1_i1,w2,w11,okay)),
  ev w11 (evn(ne1,ne0,o2_i2,w1,w14,okay)),
  ev w2  (evn(ne1,ne2,o1_i1,w3,w12,con1)),
  ev w12 (evn(ne2,ne1,o2_i2,w2,w11,con1)),
  ev w3  (evn(ne2,ne3,o1_i1,w4,w13,okay)),
  ev w13 (evn(ne3,ne2,o2_i2,w3,w12,okay)),
  ev w4  (evn(ne3,ne0,o1_i1,w1,w14,okay)),
  ev w14 (evn(ne0,ne3,o2_i2,w4,w13,okay)),
  ev_choice con [ fn() => (con1 := Con false; act con),
                  fn() => (con1 := Con true; act con)
                ]
]
val _ = (
  act w1; act con; act ck;
  reach_test :=
  ( fn init =>
    let
      val getq = fn Ne_vf ne => ne.q(#var ne)
      val q0 = getq ne0
      val rec all_eq = fn
        [] => false | [x] => x = q0 | x::xs => x = q0 andalso all_eq xs
    in
      if all_eq [getq ne1,getq ne2,getq ne3]
      then
      ( print "Clock loop detected!\n";
        backtrace();
        BasicIO.exit 0
      ) else ()
    end
  )
)
val print_comp = fn
  Clock{ql=n} => pr.printq `ck1(ql=^(pr.d n)) `
| Ne d =>
  let val r=ref(Ne d) in
    pr.printq `^(ne.id r)(q=^(pr.d(ne.q r)) `;
    pr.printq `o1=^(pr.d(#ql(ne.out1 r))) o2=^(pr.d(#ql(ne.out2 r)))) `
  end
| Con on => pr.printq `con1(^(if on then "on" else "off")) `

end end





4


