% DEFAULT_XTL_LIBRARIES="actl.xtl, ltac.xtl, macros.xtl"

-------------------------------------------------------------------------------
-- Definition of six correctness properties
-------------------------------------------------------------------------------

property XTL_PROPERTY_1 (SPEC)
    "All the REQUEST actions should have strictly positive amounts"
is
    "$SPEC.bcg" |= with xtl
	PRINT_BOOLEAN (
	    not (exists L : label in
	         L -> [ REQUEST _ _ ?amt : natural where amt <= 0 ]
	    end_exists)
	);
    expected TRUE
end property

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

property XTL_PROPERTY_2 (SPEC)
    "Between two subsequent REQUEST actions with the same reference ref"
    "(0 <= ref <= M_r), a CANCEL action with parameter ref shall appear"
is
    "$SPEC.bcg" |= with xtl
	PRINT_FORMULA (
	    forall ref : natural among { 0 ... M_r } in
		Box (isRequest (ref),
		     AG_A (not (isCancel (ref)), Box (isRequest (ref), false)
	             ))
	    end_forall
	);
    expected TRUE
end property

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

property XTL_PROPERTY_3 (SPEC)
    "A cancel of a reference 0<= ref <= M_r can appear only if a request of"
    "reference ref has been done"
is
    "$SPEC.bcg" |= with xtl
	PRINT_FORMULA (
	    INIT implies forall ref : natural among { 0 ... M_r } in
		 AG_A (not (isRequest (ref)), Box (isCancel (ref), false)
	              )
	    end_forall
	);
    expected TRUE
end property

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

property XTL_PROPERTY_4 (SPEC)
    "An order request is eventually invoiced if not cancelled (this property"
    "may be checked only on the NPOD scenarios)"
is 
    "$SPEC.bcg" |= with xtl
        PRINT_FORMULA (
            INIT implies forall ref : natural among { 0 ... M_r } in
                Box (isRequest (ref),
                        FAIR (not (isCancel (ref)), isInvoice (ref))
                )
            end_forall
        );
    expected TRUE
end property

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

property XTL_PROPERTY_5 (SPEC)
    "The protocol should be deadlock free"
is
    "$SPEC.bcg" |= with xtl
	PRINT_FORMULA (
	    not (DEADLOCK)
	);
    expected TRUE
end property

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

property XTL_PROPERTY_6 (SPEC)
    "Livelock (tau-circuit) freedom"
is
    "$SPEC.bcg" |= with xtl
	PRINT_FORMULA (
	    not (LIVELOCK)
	);
    expected TRUE
end property

-------------------------------------------------------------------------------
-- Verification of the correctness properties on different scenarios
-------------------------------------------------------------------------------

% for V in d p
% do
   % for M_p in 0   # or: M_p in 0 1 (if one wants to attack a larger problem)
   % do
      % for M_r in 1 2
      % do
         % for M_a in 1 2
         % do

            % N="p${M_p}_r${M_r}_a${M_a}"

            -- check that the LNT and LOTOS specifications are equivalent

            "inv2${V}_${N}.bcg" = generation of "inv2${V}_${N}.lnt" ;
            % cd LOTOS
            "inv2${V}_${N}.bcg" = generation of "inv2${V}_${N}.lotos" ;
            % cd ..
            strong comparison "inv2${V}_${N}.bcg" == "LOTOS/inv2${V}_${N}.bcg" ;

            -- check that the LNT specification satisfies the XTL properties

            "inv2${V}_${N}.bcg" = strong reduction of "inv2${V}_${N}.bcg" ;
            check XTL_PROPERTY_1 ("inv2${V}_${N}");
            check XTL_PROPERTY_2 ("inv2${V}_${N}");
            check XTL_PROPERTY_3 ("inv2${V}_${N}");
            -- XTL_PROPERTY_4 is not checked on this scenario
            check XTL_PROPERTY_5 ("inv2${V}_${N}");

            % SVL_RECORD_FOR_CLEAN "inv2${V}_${N}.bcg"
            % SVL_RECORD_FOR_CLEAN "LOTOS/inv2${V}_${N}.bcg"

            % if test $V = d
            % then

               -- check that the LNT and LOTOS specifications are equivalent

               "inv2d_safety_${N}.bcg" = generation of "inv2d_safety_${N}.lnt" ;
               % cd LOTOS
               "inv2d_safety_${N}.bcg" = generation of "inv2d_safety_${N}.lotos" ;
               % cd ..
               strong comparison "inv2d_safety_${N}.bcg" == "LOTOS/inv2d_safety_${N}.bcg" ;

               -- check that the LNT specification satisfies the XTL properties

               % SVL_RECORD_FOR_CLEAN "inv2d_safety_${N}.bcg"
               % SVL_RECORD_FOR_CLEAN "LOTOS/inv2d_safety_${N}.bcg"

            % fi

            % if test $V = p
            % then

               -- check that the LNT and LOTOS specifications are equivalent

               "inv2p_new_${N}.bcg" = generation of "inv2p_new_${N}.lnt" ;
               % cd LOTOS
               "inv2p_new_${N}.bcg" = generation of "inv2p_new_${N}.lotos" ;
               % cd ..
               strong comparison "inv2p_new_${N}.bcg" == "LOTOS/inv2p_new_${N}.bcg" ;

               -- check that the LNT specification satisfies the XTL properties

               "inv2p_new_${N}.bcg" = strong reduction of "inv2p_new_${N}.bcg";
               check XTL_PROPERTY_1 ("inv2p_new_${N}");
               check XTL_PROPERTY_2 ("inv2p_new_${N}");
               check XTL_PROPERTY_3 ("inv2p_new_${N}");
               check XTL_PROPERTY_4 ("inv2p_new_${N}");
               check XTL_PROPERTY_5 ("inv2p_new_${N}");

               % SVL_RECORD_FOR_CLEAN "inv2p_new_${N}.bcg"
               % SVL_RECORD_FOR_CLEAN "LOTOS/inv2p_new_${N}.bcg"

               % if test $M_p = 0
               % then

                  % echo
                  % echo "Checking safety equivalence of the initial version"
                  % echo "--------------------------------------------------"

                  "${N}_diag1.seq" = safety comparison
                     "inv2d_${N}.bcg" == "inv2p_${N}.bcg";

                  "${N}_diag2.seq" = safety comparison
                     "inv2d_${N}.bcg" <= "inv2p_${N}.bcg";

                  % echo
                  % echo "Checking safety equivalence of the modified version"
                  % echo "---------------------------------------------------"

                  "${N}_diag3.seq" = safety comparison
                     strong reduction of generation of "inv2d_safety_${N}.lnt"
                     == "inv2p_${N}.bcg";

               % fi

            % fi

         % done
      % done
   % done
% done

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