-------------------------------------------------------------------------------
(*
 * Step 1: an LTS model is generated from the specification "cim.lnt" using
 * the LNT2LOTOS, CAESAR.ADT, and CAESAR compilers. This LTS is then minimized 
 * modulo strong equivalence using BCG_MIN; this preserves the truth values 
 * of temporal logic formulas to be applied later. The resulting LTS is named 
 * "cim.bcg". We compare it against the LTS generated from the original LOTOS
 * specification to make sure that the LOTOS and LNT specifications are
 * behaviourally equivalent
 *)
-------------------------------------------------------------------------------

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

% (cd LOTOS ; echo "" ; svl)

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

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

-------------------------------------------------------------------------------
(*
 * Step 2: the 10 MCL properties characterizing the proper functioning of the 
 * cim architecture are verified in turn. Each property is explained informally
 * and is specified in both MCL V3 (dataless formula) and MCL V4 (value-passing
 * formula) as a temporal formula. Dataless formulas are checked on "cim.bcg",
 * whereas value-passing formulas are checked on a version in which the labels
 * have been renamed for convenience, named "cim_ren.bcg".
 *)
-------------------------------------------------------------------------------

"cim_ren.bcg" =
    total rename
        "\(.*\)![PR] (\([0-9]*\))\(.*\)" -> "\1!\2\3",
        "\(.*\)!CONS (P (\([0-9]*\)), \([0-9]*\), CONS (P (\([0-9]*\)), \([0-9]*\), CONS (P (\([0-9]*\)), \([0-9]*\), NIL)))" -> "\1!\2 !\3 !\4 !\5 !\6 !\7"
    in "cim.bcg";

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

property PROP_01
    "There is no deadlock in the system."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
	[ true* ] < true > true;
    expected TRUE;

    -- value-passing formula (same as dataless formula for this property)
    "cim_ren.bcg" |= with evaluator
        [ true* ] < true > true;
    expected TRUE
end property

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

% DEFAULT_MCL_LIBRARIES="standard.mcl"

property PROP_02
    "Initially, no product can be delivered before a corresponding request"
    "has been received."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        NEVER (
            ((not "REQUEST !1 !1")* . "OUTPUT !P (1) !1") |
            ((not "REQUEST !1 !2")* . "OUTPUT !P (1) !2") |
            ((not "REQUEST !1 !3")* . "OUTPUT !P (1) !3") |
            ((not "REQUEST !2 !1")* . "OUTPUT !P (2) !1") |
            ((not "REQUEST !2 !2")* . "OUTPUT !P (2) !2") |
            ((not "REQUEST !2 !3")* . "OUTPUT !P (2) !3") |
            ((not "REQUEST !3 !1")* . "OUTPUT !P (3) !1") |
            ((not "REQUEST !3 !2")* . "OUTPUT !P (3) !2") |
            ((not "REQUEST !3 !3")* . "OUTPUT !P (3) !3")
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	forall PrType:Nat among { 1 ... 3 }, Qty:Nat among { 1 ... 2 } .
	    NEVER (
                (not { REQUEST !PrType !Qty })* . { OUTPUT !PrType !Qty }
	    );
    expected TRUE
end property

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

property PROP_03
    "Every request for a product is eventually followed by the delivery of"
    "the desired quantity of that product."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        [ true* ] (
            [ "REQUEST !1 !1" ] INEVITABLE ("OUTPUT !P (1) !1") and
            [ "REQUEST !1 !2" ] INEVITABLE ("OUTPUT !P (1) !2") and
            [ "REQUEST !2 !1" ] INEVITABLE ("OUTPUT !P (2) !1") and
            [ "REQUEST !2 !2" ] INEVITABLE ("OUTPUT !P (2) !2") and
            [ "REQUEST !3 !1" ] INEVITABLE ("OUTPUT !P (3) !1") and
            [ "REQUEST !3 !2" ] INEVITABLE ("OUTPUT !P (3) !2")
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	AFTER_1_INEVITABLE_2 (
            { REQUEST ?PrType:Nat ?Qty:Nat },
            { OUTPUT !PrType !Qty }
        );
    expected TRUE
end property

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

property PROP_04
    "Since the store has a capacity of two items per product and each request"
    "asks for at least one product item, at most two requests for a product"
    "can be handled without taking a new corresponding raw material meanwhile."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        NEVER (
            true* .
            (* Two requests may occur, but three requests cannot *)
            'REQUEST !1 .*' .
            (not ('REQUEST !1 .*' or 'OUTPUT !P (1) .*' or "INPUT !1"))* .
            'REQUEST !1 .*' .
            (not ('REQUEST !1 .*' or 'OUTPUT !P (1) .*' or "INPUT !1"))* .
            'REQUEST !1 .*' .
            (not ('REQUEST !1 .*' or 'OUTPUT !P (1) .*' or "INPUT !1"))* .
            'OUTPUT !P (1) .*' .
            (not ('REQUEST !1 .*' or 'OUTPUT !P (1) .*' or "INPUT !1"))* .
            'OUTPUT !P (1) .*'
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	forall PrType:Nat among { 1 ... 3 } .
	    NEVER (
		true* .
		(* Two requests can be handled without input, but not three *)
		(
		    { REQUEST !PrType ?any } .
		    (not ({ REQUEST !PrType ?any } or { INPUT !PrType }))* .
		    { OUTPUT !PrType ?any }
		) { 3 }
	    );
    expected TRUE
end property

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

property PROP_05
    "The store is initially full (every initial product request can be"
    "fulfilled without activating the production cells), but at any moment may"
    "potentially become empty."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        [ (not 'REQUEST.*')* ] (
            [ "REQUEST !1 !1" ]
                ALWAYS_1_UNTIL_2 (not 'CMD .*', "OUTPUT !P (1) !1") and
            [ "REQUEST !1 !2" ]
                ALWAYS_1_UNTIL_2 (not 'CMD .*', "OUTPUT !P (1) !2") and
            [ "REQUEST !2 !1" ]
                ALWAYS_1_UNTIL_2 (not 'CMD .*', "OUTPUT !P (2) !1") and
            [ "REQUEST !2 !2" ]
                ALWAYS_1_UNTIL_2 (not 'CMD .*', "OUTPUT !P (2) !2") and
            [ "REQUEST !3 !1" ]
                ALWAYS_1_UNTIL_2 (not 'CMD .*', "OUTPUT !P (3) !1") and
            [ "REQUEST !3 !2" ]
                ALWAYS_1_UNTIL_2 (not 'CMD .*', "OUTPUT !P (3) !2")
        )
        and
        [ true* ]
        <
          true* .
          "CMD_ST !READ !CONS (P (1), 0, CONS (P (2), 0, CONS (P (3), 0, NIL)))"
        > true;
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	[ (not { REQUEST ?any ?any })* . { REQUEST ?PrType:Nat ?Qty:Nat } ]
	    ALWAYS_1_UNTIL_2 (not { CMD ?any ?any }, { OUTPUT !PrType !Qty })
	and
	[ true* ] < true* . { CMD_ST !"READ" ?any !0 ?any !0 ?any !0 } > true;
    expected TRUE
end property

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

property PROP_06
    "Each time a workcell is activated, it will eventually make, one by one,"
    "the requested quantity of products."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        [ true* ] (
            [ "CMD !1 !1" ] INEVITABLE ("PUT !P (1)")
            and
            [ "CMD !1 !2" ] INEVITABLE_1_THEN_2 ("PUT !P (1)", "PUT !P (1)")
            and
            [ "CMD !2 !1" ] INEVITABLE ("PUT !P (2)")
            and
            [ "CMD !2 !2" ] INEVITABLE_1_THEN_2 ("PUT !P (2)", "PUT !P (2)")
            and
            [ "CMD !3 !1" ] INEVITABLE ("PUT !P (3)")
            and
            [ "CMD !3 !2" ] INEVITABLE_1_THEN_2 ("PUT !P (3)", "PUT !P (3)")
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	[ true* . { CMD ?PrType:Nat ?Qty:Nat } ]
	    INEVITABLE_1_TIMES_2 ({ PUT !PrType }, Qty);
    expected TRUE
end property

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

property PROP_07
    "After receiving a command, a workcell cannot make a product before being"
    "fed with a corresponding raw material."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        [ true* ] (
            NEVER ('CMD !1 .*' . (not "GET !R (1)")* . "PUT !P (1)") and
            NEVER ('CMD !2 .*' . (not "GET !R (2)")* . "PUT !P (2)") and
            NEVER ('CMD !3 .*' . (not "GET !R (3)")* . "PUT !P (3)")
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	NEVER (
	    true* . { CMD ?PrType:Nat ?any } .
	    (not { GET !PrType })* . { PUT !PrType }
	);
    expected TRUE
end property

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

property PROP_08
    "Once the store is empty, the delivery corresponding to a product request"
    "cannot occur before the workcell involved has successfully executed the"
    "production command."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        NEVER (
            true* .
            (* Empty store *)
            "CMD_ST !READ !CONS (P (1), 0, CONS (P (2), 0, CONS (P (3), 0, NIL)))" .
            (
                ('REQUEST !1 .*' . (not "RDY !1")* . 'OUTPUT !P (1) .*') |
                ('REQUEST !2 .*' . (not "RDY !2")* . 'OUTPUT !P (2) .*') |
                ('REQUEST !3 .*' . (not "RDY !3")* . 'OUTPUT !P (3) .*')
            )
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	NEVER (
	    (* Empty store *)
	    true* . { CMD_ST !"READ" ?any !0 ?any !0 ?any !0 } .
	    { REQUEST ?PrType:Nat ?any } . (not { RDY !PrType })* .
	    { OUTPUT !PrType ?any }
	);
    expected TRUE
end property

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

property PROP_09
    "Every time the store does not contain sufficient products to fulfill a"
    "request, there will be supply demands for the corresponding raw material."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        [ true* ] (
            (* Product of type 1 *)
            [
                "REQUEST !1 !1" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (1), 0.*'
            ] INEVITABLE ("INPUT !1")
            and
            [
                "REQUEST !1 !2" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (1), 0.*'
            ] INEVITABLE_1_THEN_2 ("INPUT !1", "INPUT !1")
            and
            [
                "REQUEST !1 !2" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (1), 1.*'
            ] INEVITABLE ("INPUT !1")
            and
            (* Product of type 2 *)
            [
                "REQUEST !2 !1" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (2), 0.*'
            ] INEVITABLE ("INPUT !2")
            and
            [
                "REQUEST !2 !2" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (2), 0.*'
            ] INEVITABLE_1_THEN_2 ("INPUT !2", "INPUT !2")
            and
            [
                "REQUEST !2 !2" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (2), 1.*'
            ] INEVITABLE ("INPUT !2")
            and
            (* Product of type 3 *)
            [
                "REQUEST !3 !1" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (3), 0.*'
            ] INEVITABLE ("INPUT !3")
            and
            [
                "REQUEST !3 !2" .
                (not 'REQUEST .*')* .
                'CMD_ST !READ !.*P (3), 0.*'
            ] INEVITABLE_1_THEN_2 ("INPUT !3", "INPUT !3")
            and
            [
                "REQUEST !3 !2" .
                (not 'REQUEST .*')* . 
                'CMD_ST !READ !.*P (3), 1.*'
            ] INEVITABLE ("INPUT !3")
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	[
	    true* . { REQUEST ?PrType:Nat ?Qty:Nat } .
	    (not { REQUEST ?any ?any })* .
	    { CMD_ST !"READ" ?any ?Qty_1:Nat ?any ?Qty_2:Nat ?any ?Qty_3:Nat }
	] (
	    (((PrType = 1) and (Qty_1 = 0)) or
	     ((PrType = 2) and (Qty_2 = 0)) or
	     ((PrType = 3) and (Qty_3 = 0)))
	    implies
	    INEVITABLE_1_TIMES_2 ({ INPUT !PrType }, Qty)
	);
    expected TRUE
end property

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

property PROP_10
    "Every time a workcell receives a command for a product, the two transport"
    "belts will be inevitably started to carry the raw material and the"
    "product."
is
    -- dataless formula
    "cim.bcg" |= with evaluator
        [ true* ] (
            [ 'CMD !1 .*' ] INEVITABLE_1_THEN_2 ('WIN !1 .*', "WOUT !P (1)")
            and
            [ 'CMD !2 .*' ] INEVITABLE_1_THEN_2 ('WIN !2 .*', "WOUT !P (2)")
            and
            [ 'CMD !3 .*' ] INEVITABLE_1_THEN_2 ('WIN !3 .*', "WOUT !P (3)")
        );
    expected TRUE;

    -- value-passing formula
    "cim_ren.bcg" |= with evaluator
	[ true* . { CMD ?PrType:Nat ?any } ]
	    INEVITABLE_1_THEN_2 ({ WIN !PrType ?any }, { WOUT !PrType });
    expected TRUE
end property

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