% DEFAULT_PROCESS_FILE=odp.lnt (* all processes are defined in file "odp.lnt" *) (* * generation of the state space of the whole system * * the state space of the trader is generated using an interface that * takes into account the environment constraints imposed on the trader by * three of the four objects *) "odp.bcg" = generation of leaf strong reduction of hide all but WORK in par EXPORT, IMPORT in (refined abstraction Object_1, Object_2, Object_3 using "Trader_Alphabet" of "Trader") || par WORK #2 in Object_1 || Object_2 || Object_3 || Object_4 end par end par; ------------------------------------------------------------------------------- (* * we also generate the state space for the original LOTOS specification and we * compare it against the state space generated from the LNT specification, to * make sure that the LOTOS and LNT specifications are behaviourally equivalent *) % (cd LOTOS ; echo "" ; svl) "diag.bcg" = strong comparison "odp.bcg" == "LOTOS/odp.bcg"; % SVL_COMMAND_FOR_CLEAN "(cd LOTOS ; svl -clean)" ------------------------------------------------------------------------------- property PROP_A "The system has no livelock" is -- this property is checked before minimizing livelock.bcg modulo -- branching bisimulation (which eliminates livelocks) "livelock.bcg" = livelock of "odp.bcg"; expected FALSE end property ------------------------------------------------------------------------------- "odp.bcg" = branching reduction of "odp.bcg"; ------------------------------------------------------------------------------- property PROP_B "In every state, every object can eventually execute the services of" "which it is a client" is "diag.bcg" = "odp.bcg" |= [true*] ( ( true) and ( true) and ( true) and ( true) and ( true) and ( true) and ( true) and ( true)); expected TRUE end property ------------------------------------------------------------------------------- property PROP_C (I) "The object \"O$I\" executes the expected services independently of the" "other services" is -- the verification is done on-the-fly "diag.seq" = branching comparison total rename "WORK !.* !.* \(!.*\)" -> "WORK \1" in total hide all but "WORK !.* !O$I !.*" in "odp.bcg" == "Object_${I}_Service"; expected TRUE end property % for I in 1 2 3 4 % do check PROP_C ("$I"); % done -------------------------------------------------------------------------------