(*
 * The BCG graph corresponding to the LNT specification "overtaking.lnt"
 * is generated.
 *)

"overtaking.bcg" = generation of "overtaking.lnt";

------------------------------------------------------------------------------

(*
 * This BCG graph is compared (modulo strong equivalence) against the BCG
 * graph generated from the original LOTOS specification, in order to show
 * that both the LNT and LOTOS specifications are behaviourally equivalent.
 *)

% (cd LOTOS ; echo "" ; svl)

"diag.bcg" = strong comparison "overtaking.bcg" == "LOTOS/overtaking.bcg";

% SVL_COMMAND_FOR_CLEAN "(cd LOTOS ; svl -clean)"

------------------------------------------------------------------------------

(*
 * Label hiding and renaming is applied to the BCG graph in order to
 * compute an abstract version of the protocol, that only refers to the
 * actions needed for verification. Precisely, some labels are renamed in
 * order to abstract away the vehicle brand information (second offer),
 * while all the other labels are hidden. The resulting graph is then reduced
 * for strong bisimulation and stored in file "overtaking.bcg".
 *)

"overtaking.bcg" = strong reduction of
		   total hide all but
		     "S !OT_BEGIN !TAIL",
		     "S !OT_BEGIN !MIDDLE",
		     "S !OT_END !TAIL"
		   in total rename
		     "S !OT_BEGIN !.* !MIDDLE" -> "S !OT_BEGIN !MIDDLE",
		     "S !OT_BEGIN !.* !TAIL" -> "S !OT_BEGIN !TAIL",
		     "S !OT_END !.* !TAIL" -> "S !OT_END !TAIL"
		   in "overtaking.bcg";

------------------------------------------------------------------------------

property Safety_Property_1
   "A vehicle can overtake only if there is no vehicle already overtaking it."
is
   (*
    * Using the notations of the LNT description, this can be rephrased as:
    * "When the TAIL vehicle is commited into an overtaking, the vehicle in
    * MIDDLE position cannot overtake unless the TAIL vehicle terminates".
    * Verification is done using equivalences. The expected behaviour of the
    * system is represented by the graph stored in file "true_property.aut".
    * The graphs "overtaking.bcg" and "true_property.aut" are compared with
    * respect to safety equivalence. The comparison is computed on-the-fly.
    *)

    "diag1.seq" = safety comparison "true_property.aut" == "overtaking.bcg";
    expected TRUE
end property

------------------------------------------------------------------------------

property Safety_Property_2
   "Is there a sequence in which the above property is violated?"
is
   (*
    * Such an undesirable sequence is expressed by the graph stored in
    * file "false_property.aut". Verifying if this sequence is possible is
    * done by comparing "overtaking.hide" and "false_property.aut" with
    * respect to tau*.a preorder.
    *)

    "diag2.seq" = tau*.a comparison "false_property.aut" <= "overtaking.bcg";
    expected FALSE
end property

------------------------------------------------------------------------------