(* * The BCG graphs corresponding to the LNT specification of the INRES service * and protocol are generated first. *) "inres_service_int.bcg" = generation of "inres_service_int.lnt"; "inres_protocol_int_6.bcg" = generation of "inres_protocol_int_6.lnt"; ------------------------------------------------------------------------------ (* * These BCG graphs are compared (modulo strong equivalence) against the BCG * graphs generated from the LOTOS specifications, in order to show that * the LNT and LOTOS specifications are pairwise behaviourally equivalent. *) % (cd LOTOS ; echo "" ; svl) "diag1.bcg" = strong comparison "inres_service_int.bcg" == "LOTOS/inres_service_int.bcg"; "diag2.bcg" = strong comparison "inres_protocol_int_6.bcg" == "LOTOS/inres_protocol_int_6.bcg"; % SVL_COMMAND_FOR_CLEAN "(cd LOTOS ; svl -clean)" ------------------------------------------------------------------------------ (* * The BCG graphs of the service and the protocol can be compared wrt safety * equivalence or wrt safety preorder. BISIMULATOR points out that the service * is not safety equivalent to the protocol, and gives distinguishing * sequences in file diag3.bcg, diag4.bcg, and diag5.bcg. *) "diag3.bcg" = safety comparison "inres_service_int.bcg" == "inres_protocol_int_6.bcg"; "diag4.bcg" = safety comparison "inres_service_int.bcg" <= "inres_protocol_int_6.bcg"; "diag5.bcg" = safety comparison "inres_service_int.bcg" >= "inres_protocol_int_6.bcg"; ------------------------------------------------------------------------------ (* * One can also check whether some execution sequences, derived from the * graphical Message Sequence Charts (MSC) of the INRES protocol, are * accepted by version 6 of the protocol. *) % echo '' % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_1.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_2.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_3.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_4.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_5.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_6.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_7.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_8.seq % bcg_open inres_protocol_int_6.bcg exhibitor < sequence_9.seq (* * The same verifications can also be done on-the-fly, without generating * inres_protocol_int_6.bcg first. *) % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_1.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_2.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_3.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_4.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_5.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_6.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_7.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_8.seq % lnt.open inres_protocol_int_6.lnt exhibitor < sequence_9.seq ------------------------------------------------------------------------------ (* * One can use the TGV tool to generate test cases on the fly for the INRES * service, according to the test purpose specified in inres_service_tp.aut. *) % lnt.open inres_service_int.lnt tgv -csg -io inres_service_int.io -output test.bcg -unlock inres_service_tp.aut ------------------------------------------------------------------------------