(*
 * This SVL script performs the following activities:
 * - generation of the LTS corresponding to "peterson.lnt" and minimization
 *   modulo strong bisimulation of the resulting LTS; this results in an LTS
 *   file named "peterson.bcg"
 * - verification on "peterson.bcg" of temporal-logic formulas using the XTL
 *   and EVALUATOR model checkers
 * - verification that both LTSs for the LOTOS and LNT versions are strongly
 *   bisimilar
 *)

"peterson.bcg" = strong reduction of generation of "peterson.lnt";

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

% DEFAULT_XTL_LIBRARIES="ltac.xtl"
% DEFAULT_MCL_LIBRARIES="macros.mcl"

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

property PROPERTY_1
    "Deadlock freedom"
is
    "peterson.bcg" |= with xtl
        PRINT_FORMULA (not (DEADLOCK));
    expected TRUE;

    "peterson.bcg" |= with evaluator
	[ true* ] < true > true;
    expected TRUE
end property

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

property PROPERTY_2
    "Livelock (tau-circuit) freedom"
is
    "peterson.bcg" |= with xtl
        PRINT_FORMULA (not (LIVELOCK));
    expected TRUE;

    "peterson.bcg" |= with evaluator
	not < "i" > @;
    expected TRUE;
end property

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

property PROPERTY_3
    "Mutual exclusion. After Pi has entered its critical section CSi, it is"
    "not possible that Pj enters its critical section CSj until Pi has"
    "released CSi"
is
    "peterson.bcg" |= with xtl
	let
            (* Critical sections *)
            CS0      : labelset = EVAL_A (CS0),
            CS1      : labelset = EVAL_A (CS1),
            (* Release the critical sections *)
            REL0     : labelset = EVAL_A (F0 !"WRITE" !false),
            REL1     : labelset = EVAL_A (F1 !"WRITE" !false)
        in
            PRINT_FORMULA (
                NOT_TO_UNLESS (CS0, CS1, REL0)
                and
                NOT_TO_UNLESS (CS1, CS0, REL1)
            )
        end_let;
    expected TRUE;

    "peterson.bcg" |= with evaluator
	[ true* . ((CS0 . (not REL0)* . CS1) | (CS1 . (not REL1)* . CS0)) ]
	    false;
    expected TRUE
end property

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

property PROPERTY_4
    "Liveness of each process. From any state and for every action \"a\" of"
    "P0 or P1, it is possible to reach a state where \"a\" is enabled"
is
    "peterson.bcg" |= with xtl
        let
            (* Non critical sections *)
            NCS0     : labelset = EVAL_A (NCS0),
            NCS1     : labelset = EVAL_A (NCS1),
            (* Critical sections *)
            CS0      : labelset = EVAL_A (CS0),
            CS1      : labelset = EVAL_A (CS1),
            (* Request access to the critical sections *)
            REQ0     : labelset = EVAL_A (F0 !"WRITE" !true),
            REQ1     : labelset = EVAL_A (F1 !"WRITE" !true),
            (* Release the critical sections *)
            REL0     : labelset = EVAL_A (F0 !"WRITE" !false),
            REL1     : labelset = EVAL_A (F1 !"WRITE" !false),
            (* Write the TURN variable *)
            TURN_W_0 : labelset = EVAL_A (T !"WRITE" !0),
            TURN_W_1 : labelset = EVAL_A (T !"WRITE" !1),
            (* Read the variables *)
            F0_R     : labelset = EVAL_A (F0 !"READ" _),
            F1_R     : labelset = EVAL_A (F1 !"READ" _),
            TURN_R   : labelset = EVAL_A (T !"READ" _)
        in
            PRINT_FORMULA (
                POT (ENABLE (NCS0))     and	(* actions done by process 0 *)
                POT (ENABLE (CS0))      and
                POT (ENABLE (TURN_W_0)) and
                POT (ENABLE (REQ0))     and
                POT (ENABLE (REL0))     and
                POT (ENABLE (F1_R))
                and
                POT (ENABLE (NCS1))     and	(* actions done by process 1 *)
                POT (ENABLE (CS1))      and
                POT (ENABLE (TURN_W_1)) and
                POT (ENABLE (REQ1))     and
                POT (ENABLE (REL1))     and
                POT (ENABLE (F0_R)) 
                and
                POT (ENABLE (TURN_R))	(* action done by both processes *)
            )
        end_let;
    expected TRUE;

    "peterson.bcg" |= with evaluator
	[ true* ] (
	    (* actions performed by process 0 *)
	    < true* . NCS0 > true	and
	    < true* . CS0 > true	and
	    < true* . TURN_W_0 > true	and
	    < true* . REQ0 > true	and
	    < true* . REL0 > true	and
	    < true* . F1_R > true	and

	    (* actions performed by process 1 *)
	    < true* . NCS1 > true	and
	    < true* . CS1 > true	and
	    < true* . TURN_W_1 > true	and
	    < true* . REQ1 > true	and
	    < true* . REL1 > true	and
	    < true* . F0_R > true	and

	    (* actions performed by the 2 processes *)
	    < true* . TURN_R > true
	);
    expected TRUE
end property

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

property PROPERTY_5
    "Reachability of Pi's critical section if Pj does not request the access."
    "After Pi has requested the CSi and after Pj has released CSj, all paths"
    "lead either to a request of Pj (REQj) or to an access of Pi (CSi)."
is
    "peterson.bcg" |= with xtl
        let
            (* Critical sections *)
            CS0      : labelset = EVAL_A (CS0),
            CS1      : labelset = EVAL_A (CS1),
            (* Request access to the critical sections *)
            REQ0     : labelset = EVAL_A (F0 !"WRITE" !true),
            REQ1     : labelset = EVAL_A (F1 !"WRITE" !true),
            (* Release the critical sections *)
            REL0     : labelset = EVAL_A (F0 !"WRITE" !false),
            REL1     : labelset = EVAL_A (F1 !"WRITE" !false)
        in
            PRINT_FORMULA (
                Box (REQ0, ALL (Box (REL1, INEV (REQ1 or CS0))))
                and
                Box (REQ1, ALL (Box (REL0, INEV (REQ0 or CS1))))
            )
        end_let;
    expected TRUE;

    "peterson.bcg" |= with evaluator
	[ true* ] (
	    [ REQ0 . true* . REL1 ]
		mu X . (< true > true and [ not (REQ1 or CS0) ] X)
	    and
	    [ REQ1 . true* . REL0 ]
		mu X . (< true > true and [ not (REQ0 or CS1) ] X)
	);
    expected TRUE
end property

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

property PROPERTY_6
    "Reachability of both critical sections under fair scheduling of actions"
is
    "peterson.bcg" |= with xtl
        let
            (* Critical sections *)
            CS0      : labelset = EVAL_A (CS0),
            CS1      : labelset = EVAL_A (CS1)
        in
            PRINT_FORMULA (FAIR (CS0) and FAIR (CS1))
        end_let;
    expected TRUE;

    "peterson.bcg" |= with evaluator
	[ true* ] (
	    [ (not CS0)* ] < (not CS0)* . CS0 > true
	    and
	    [ (not CS1)* ] < (not CS1)* . CS1 > true
	);
    expected TRUE
end property

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

-- Checking that the LOTOS and LNT specifications are equivalent

% (cd LOTOS ; echo "" ; svl)
"diag.bcg" = strong comparison "LOTOS/peterson.bcg" == "peterson.bcg";

-- Cleaning up

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

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