(*
 * Step 1:
 * -------
 * The LNT specifications "turntable_seq.lnt" and "turntable_par.lnt", which
 * describes the turntable system equipped with a sequential and a parallel
 * controller, respectively, are first generated in BCG format.
 *
 * Then, these BCG graphs are compared (modulo strong equivalence) against
 * the BCG graphs generated from the original LOTOS specification, in order
 * to show that both the LNT and LOTOS specifications are behaviourally
 * equivalent.
 *
 * Finally, the parallel version is compared against the (simpler)
 * sequential version, equipped with a sequential controller, given in file
 * "turntable_seq.lnt". This is done by using Bisimulator to compare on the
 * fly "turntable_par.lnt" against "tt_seq.bcg" modulo branching preorder
 *)

"tt_seq.bcg" = generation of "turntable_seq.lnt";

"tt_par.bcg" = generation of "turntable_par.lnt";

% (cd LOTOS ; echo "" ; svl)

"diag_seq.bcg" = strong comparison "tt_seq.bcg" == "LOTOS/tt_seq.bcg";

"diag_par.bcg" = strong comparison "tt_par.bcg" == "LOTOS/tt_par.bcg";

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

"par_gt_seq.seq" = branching comparison "turntable_par.lnt" >= "tt_seq.bcg";

(* ========================================================================= *)

(*
 * Step 2:
 * -------
 * Satisfaction of several correctness properties (written in MCL V4) that
 * characterize the desired behaviour of the system is checked on-the-fly
 * using Evaluator on the system equipped first with the sequential, then
 * with the parallel version of the controller.
 *)

% for VERSION in turntable_seq turntable_par
% do

-- default MCL libraries for properties PROP_01 to PROP_07
% DEFAULT_MCL_LIBRARIES="standard.mcl"

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

property PROP_01 (SPEC)
    "After a product has been added and the table has rotated once, the master"
    "controller cannot send a drill command before the clamp was locked."
is
    "$SPEC.lnt" |=
	NEVER (
	    true* . "INF !PRESENT" .
	    (not "INF !TURNED")* . "INF !TURNED" .
	    (not "INF !LOCKED")* . "CMD !DRILL"
	);
    expected TRUE
end property

check PROP_01 ("$VERSION");

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

property PROP_02 (SPEC)
    "After a product has been drilled, the master controller cannot send"
    "a turn command before the clamp was unlocked."
is
    "$SPEC.lnt" |=
        NEVER (
	    true* . "INF !DRILLED" .
	    (not "INF !UNLOCKED")* . "CMD !TURN"
	);
    expected TRUE
end property

check PROP_02 ("$VERSION");

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

property PROP_03 (SPEC)
    "After the clamp has been unlocked and the table has rotated once, the"
    "master controller cannot send a turn command before a product was tested."
is
    "$SPEC.lnt" |=
        NEVER (
  	    true* . "INF !UNLOCKED" .
	    (not "INF !TURNED")* . "INF !TURNED" .
	    (not 'INF !TESTED.*')* . "CMD !TURN"
	);
    expected TRUE
end property

check PROP_03 ("$VERSION");

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

property PROP_04 (SPEC)
    "After a product has been tested and the table has rotated once, the"
    "master controller cannot send a turn command before the product was"
    "delivered."
is
    "$SPEC.lnt" |=
        NEVER (
	    true* . 'INF !TESTED.*' .
	    (not "INF !TURNED")* . "INF !TURNED" .
	    (not "INF !ABSENT")* . "CMD !TURN"
	);
    expected TRUE
end property

check PROP_04 ("$VERSION");

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

property PROP_05 (SPEC)
    "After a product has been delivered and the table has rotated once, the"
    "master controller cannot send a turn command before a product was added."
is
    "$SPEC.lnt" |=
	NEVER (
	    true* . "INF !ABSENT" .
	    (not "INF !TURNED")* . "INF !TURNED" .
	    (not "INF !PRESENT")* . "CMD !TURN"
	);
    expected TRUE
end property

check PROP_05 ("$VERSION");

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

property PROP_06 (SPEC)
    "Each time the testing device detects a good product, no error will be"
    "signaled during the next processing cycle."
is
    "$SPEC.lnt" |=
        NEVER (
	    true* .
	    "INF !TESTED !TRUE" .
	    (not "INF !TURNED")* . "INF !TURNED" .
	    (not "INF !TURNED")* . "ERR"
	);
    expected TRUE
end property

check PROP_06 ("$VERSION");

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

property PROP_07 (SPEC, RESULT)
    "After the drilling and testing position of the turntable have been"
    "filled, the master controller cannot send a testing command before"
    "a drilling command"
is
    -- dataless formula
    "$SPEC.lnt" |= with evaluator3
        NEVER (
            true* . "INF !PRESENT" .
            true* . "INF !PRESENT" .
            true* . "INF !PRESENT" .
            true* .
            "CMD !TEST" . (not "INF !TURNED")* . "CMD !DRILL"
        );
    expected "$RESULT";

    -- value-passing formula
    "$SPEC.lnt" |= with evaluator4
	NEVER (
	    (true* . "INF !PRESENT") { 3 } .
	    true* .
	    "CMD !TEST" . (not "INF !TURNED")* . "CMD !DRILL"
	);
    expected "$RESULT"
end property

% case $SPEC in
%     turntable_seq )
          -- the property should be true for the sequential version
          check PROP_07 ("$VERSION", TRUE);
%     ;;
%     turntable_par )
          -- the property should be false for the parallel version
           check PROP_07 ("$VERSION", FALSE);
%     ;;
% esac

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

-- default MCL libraries for properties PROP_08 to PROP_14
% DEFAULT_MCL_LIBRARIES="actl.mcl"

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

property PROP_08 (SPEC)
    "Initially, the master controller eventually commands the addition of"
    "products on all the slots of the turntable."
is
    -- dataless formula
    "$SPEC.lnt" |= with evaluator3
        AU_A_A (true, not ("CMD !TURN"), "REQ !ADD",
            AU_A_A (true, not "CMD !TURN", "CMD !TURN",
                AU_A_A (true, not "CMD !TURN", "REQ !ADD",
                    AU_A_A (true, not "CMD !TURN", "CMD !TURN",
                        AU_A_A (true, not "CMD !TURN", "REQ !ADD",
                            AU_A_A (true, not "CMD !TURN", "CMD !TURN",
                                AU_A_A (true, not "CMD !TURN", "REQ !ADD", true)
                            )
                        )
                    )
                )
            )
        );
    expected TRUE;

    -- value-passing formula
    "$SPEC.lnt" |= with evaluator4
	(* first addition *)
	AU_A_A (true, not "CMD !TURN", "REQ !ADD",
	    (* followed by three turns and three additions *)
	    mu X (nb_add_turn:nat := 3) . (
		(nb_add_turn > 0) implies
		AU_A_A (true, not "CMD !TURN", "CMD !TURN",
		    AU_A_A (true, not "CMD !TURN", "REQ !ADD",
			X (nb_add_turn - 1)))
	    )
	);
    expected TRUE
end property

check PROP_08 ("$VERSION");

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

property PROP_09 (SPEC)
    "Each time a product is added, it will be drilled after the next rotation"
    "of the turntable."
is
    "$SPEC.lnt" |=
	[ true* . "INF !PRESENT" ]
	    AU_A_A (true, not "CMD !TURN", "CMD !TURN",
	        AU_A_A (true, not "CMD !TURN", "CMD !LOCK",
	            AU_A_A (true, not "CMD !TURN", "CMD !DRILL",
	                AU_A_A (true, not "CMD !TURN", "CMD !UNLOCK", true)
	            )
	        )
	    );
    expected TRUE
end property

check PROP_09 ("$VERSION");

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

property PROP_10 (SPEC)
    "Each time the clamp is released, the corresponding product will be tested"
    "after the next rotation of the turntable."
is
    "$SPEC.lnt" |=
	[ true* . "INF !UNLOCKED" ]
	    AU_A_A (true, not "CMD !TURN", "CMD !TURN",
	        AU_A_A (true, not "CMD !TURN", "CMD !TEST", true)
	    );
    expected TRUE
end property

check PROP_10 ("$VERSION");

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

property PROP_11 (SPEC)
    "Each time a product is tested, it will be delivered after the next"
    "rotation of the turntable."
is
    "$SPEC.lnt" |=
	[ true* . 'INF !TESTED.*' ]
	    AU_A_A (true, not "CMD !TURN", "CMD !TURN",
	        AU_A_A (true, not "CMD !TURN", 'REQ !REMOVE.*', true)
	    );
    expected TRUE
end property

check PROP_11 ("$VERSION");

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

property PROP_12 (SPEC)
    "Each time a product is delivered, another one will be added after the"
    "next rotation of the turntable."
is
    "$SPEC.lnt" |=
	[ true* . "INF !ABSENT" ]
	    AU_A_A (true, not "CMD !TURN", "CMD !TURN",
	        AU_A_A (true, not "CMD !TURN", "REQ !ADD", true)
	    );
    expected TRUE
end property

check PROP_12 ("$VERSION");

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

property PROP_13 (SPEC)
    "Each command (resp. request) sent by the master controller to the devices"
    "(resp. to the environment) is eventually followed by its acknowledgement"
    "before the turntable has rotated."
is
    "$SPEC.lnt" |=
	[ true* ] (
	    [ "REQ !ADD" ]
		AU_A_A (true, not "INF !TURNED", "INF !PRESENT", true)
	    and
	    [ "CMD !LOCK" ]
		AU_A_A (true, not "INF !TURNED", "INF !LOCKED", true)
	    and
	    [ "CMD !DRILL" ]
		AU_A_A (true, not "INF !TURNED", "INF !DRILLED", true)
	    and
	    [ "CMD !UNLOCK" ]
		AU_A_A (true, not "INF !TURNED", "INF !UNLOCKED", true)
	    and
	    [ "CMD !TEST" ]
		AU_A_A (true, not "INF !TURNED", 'INF !TESTED.*', true)
	    and
	    [ 'REQ !REMOVE.*' ]
		AU_A_A (true, not "INF !TURNED", "INF !ABSENT", true)
	    and
	    [ "CMD !TURN" ]
		AU_A_A (true, not "INF !TURNED", "INF !TURNED", true)
	);
    expected TRUE
end property

check PROP_13 ("$VERSION");

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

property PROP_14 (SPEC)
    "Each time the testing device detects a faulty product, the error will be"
    "eventually signaled during the next processing cycle."
is
    "$SPEC.lnt" |=
	[ true* . "INF !TESTED !FALSE" ]
	    AU_A_A (true, not "CMD !TURN", "CMD !TURN",
	        AU_A_A (true, not "CMD !TURN", "ERR", true)
	    );
    expected TRUE
end property

check PROP_14 ("$VERSION");

% done

(* ========================================================================= *)

(*
 * Step 3:
 * -------
 * Performance evaluation of the turntable system equipped with the
 * sequential and parallel version of the controller is performed using
 * Determinator, Bcg_Min, and Bcg_Steady. The resulting file "turntable.ps"
 * contains the graphical representation of the product delivery throughput.
 *)

"tt_par.bcg" = generation of "turntable_par.lnt";

% REMOVE_DELAY=100.0

% for CONTROLLER in "seq" "par"
% do
      % echo
      % echo "*** Analyzing turntable with ${CONTROLLER} controller"

      "tt_${CONTROLLER}_1.bcg" = branching reduction of
          hide all but LAMBDA, MU, NU in
              "tt_${CONTROLLER}.bcg";

      % for PROCESSING_DELAY in 0.5 1.0 2.0
      % do

          % echo
          % echo "+++ Processing delay ${PROCESSING_DELAY}"

          % DATA="tt_${CONTROLLER}_${PROCESSING_DELAY}.thr"
          % rm -f $DATA

          % for LOAD in 0.1 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1.0
          % do
                "tt_${CONTROLLER}_2.bcg" = total rename
                      "LAMBDA"         -> "REMOVE; rate $REMOVE_DELAY",
                      "NU"             -> "rate $LOAD",
                      "MU !TURNED"     -> "TURN; rate $PROCESSING_DELAY",
                      "MU !DRILLED"    -> "DRILL; rate $PROCESSING_DELAY",
                      "MU !TESTED"     -> "TEST; rate $PROCESSING_DELAY"
                    in "tt_${CONTROLLER}_1.bcg";

                % bcg_open "tt_${CONTROLLER}_2.bcg" determinator "tt_${CONTROLLER}_3.bcg"
                % bcg_info -size "tt_${CONTROLLER}_3.bcg"

                (* check the absence of tau transitions *)
                % bcg_info -hidden "tt_${CONTROLLER}_3.bcg"

                (* compute throughput *)
                % bcg_steady -thr -append $DATA "tt_${CONTROLLER}_3.bcg" LOAD=$LOAD
          % done
      % done
% done

(* calling Gnuplot to generate turntable.ps *)
% gnuplot turntable.plot

(* displaying the Postscript file generated by Gnuplot *)
% "$CADP"/src/com/cadp_postscript turntable.ps

(* cleanup *)
% $CADP/src/com/cadp_rm determinator
% for FILE in tt_*_*.bcg tt_*_*.thr turntable.ps
% do
%       SVL_RECORD_FOR_CLEAN "$FILE"
% done

(* ========================================================================= *)