Workspaces ---- apbd asves asvpapers bear blast buildmaster caltrop cases compaan concurrency cosi dif diva dopcenter dopsysadmin elab embedded embeddedadmin giotto healtheu hyinfo m2t2 mescal metropolis mica mobies mocpaper msgadmin mvsis nephest platform ransom robosysadmin savg sec seminar sensorprivacy smartnets systems truck video webmaster wow

Tasting Mocha: Counter
For editing use the mouse to cut and paste. Use the mouse to select a position and type in your changes. System definition: A set of reactive modules -- this is a comment -- 3 bit counter found in the SMV example suite module counterCell private sumBit : bool external carryIn : bool interface carryOut : bool atom controls sumBit reads sumBit awaits carryIn init [] true -> sumBit' := false update [] ~sumBit -> sumBit' := carryIn' [] sumBit -> sumBit' := if (~carryIn') then true else false fi endatom atom controls carryOut reads sumBit awaits carryIn init [] true -> carryOut' := false update [] true -> carryOut' := sumBit & carryIn' endatom endmodule -- end counterCell cell0 := counterCell[carryIn, carryOut := input, out0] cell1 := counterCell[carryIn, carryOut := out0, out1] cell2 := counterCell[carryIn, carryOut := out1, out2] threebitcounter := hide out0, out1 in (cell0 || cell1 || cell2) endhide --------------------------------------------------------------------------------- module nondetinput interface output : bool atom controls output init update [] true -> output' := nondet endatom endmodule --------------------------------------------------------------------------------- InputModule := nondetinput[output := input] closedthreebitcounter := hide input in (InputModule || threebitcounter) endhide Specification: A list of invariants or ATL formulae atl "atl1" A F (out2); atl "atl2" E F (out2) ; atl "atl3" << InputModule >> G << InputModule >> F (out2); Model Checking: Module formulae pairs or check_refine commands atl_check closedthreebitcounter atl1 atl_check closedthreebitcounter atl2 atl_check closedthreebitcounter atl3
Last modified: ,  Hits

You are not logged in

©2002-2009 U.C. Regents