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: Peterson
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 type ctype:{outCS, reqCS, inCS} module P1 interface x1:bool; pc1:ctype external x2:bool; pc2:ctype lazy atom controls pc1,x1 reads pc1,pc2,x1,x2 init [] true -> pc1':= outCS update [] pc1 = outCS -> pc1':=reqCS; x1':= x2 [] pc1 = reqCS & (pc2 = outCS | ~(x1=x2)) -> pc1':=inCS [] pc1 = inCS -> pc1':=outCS endatom endmodule module P2 interface pc2:ctype; x2:bool external pc1:ctype; x1:bool lazy atom controls pc2,x2 reads pc1,pc2,x1,x2 init [] true -> pc2':= outCS update [] pc2 = outCS -> pc2':=reqCS; x2':= ~x1 [] pc2 = reqCS & (pc1 = outCS | x1=x2) -> pc2':=inCS [] pc2 = inCS -> pc2':=outCS endatom endmodule Pete:= hide x1, x2 in (P1 || P2) endhide Specification: A list of invariants or ATL formulae inv "mutex" ~(pc1 = inCS & pc2 = inCS); Model Checking: Module formulae pairs or check_refine commands inv_check Pete mutex
Last modified: ,  Hits

You are not logged in

©2002-2009 U.C. Regents