(*---------------------------------------------------------------------------*
 * This script checks the randomized consensus protocol for 3 processes,     *
 * 1 potentially faulty process, and NB_ROUNDS rounds.                       *
 *                                                                           *
 * In a first step, the LTS modeling one round of the consensus is generated *
 * compositionally, the system being decomposed in terms of processes and    *
 * (asynchronous) communications between processes.                          *
 *                                                                           *
 * In a second step, the LTS modeling two rounds of the consensus is         *
 * generated following the same method.                                      *
 *                                                                           *
 * Then, it is checked that the LTS modeling two rounds of the consensus can *
 * be obtained much more efficiently by composing two instances of the LTS   *
 * modeling one round, the labels of one being appropriately renamed. This   *
 * shows that the consensus protocol is compositional in terms of rounds.    *
 *                                                                           *
 * Then, using round compositionality, the LTS modeling NB_ROUNDS rounds is  *
 * generated.                                                                *
 *---------------------------------------------------------------------------*)

% DEFAULT_PROCESS_FILE="CONSENSUS.lnt"
% NB_ROUNDS=10

(*---------------------------------------------------------------------------*
 * Function GENERATE_ROUNDS generates an LTS modeling the consensus          *
 * protocol for 3 processes, 1 potential faulty process, and $1 rounds.      *
 *---------------------------------------------------------------------------*)

% GENERATE_ROUNDS () {

%   N="$1"

    "$2.bcg" = generation of leaf strong reduction of 
        total rename    (* rename LOTOS gates with offers into gates *)
            "SEND !\(.*\) !\(.*\) !\(.*\) !\(.*\) !\(.*\)" ->
                "SEND_\1_\2_\3_\4_\5",
            "RECV !\(.*\) !\(.*\) !\(.*\) !\(.*\) !\(.*\)" ->
                "RECV_\1_\2_\3_\4_\5",
            "OUTPUT !\(.*\) \(!.*\) \(!.*\)" -> "OUTPUT_\1 \2 \3",
            "DEC !\(.*\) \(!.*\)" -> "DEC \2"
        in
            INPUT_VALUES [SEND, RECV, DEC, INPUT, OUTPUT] (3, 1, 1, 1, "$N")
            |||
            INPUT_VALUES [SEND, RECV, DEC, INPUT, OUTPUT] (3, 1, 2, 1, "$N")
            |||
            INPUT_VALUES [SEND, RECV, DEC, INPUT, OUTPUT] (3, 1, 3, 1, "$N");

(* We incorporate communication media, iterating on pairs of distinct        *
 * processes (I, J) where J < I, and on rounds K.                            *)

%   for I in 1 2 3
%   do
%     J=1
%     while [ $J -lt $I ]
%     do
%       K=1
%       while [ $K -le $1 ]
%       do

(* We generate a medium with 5 places modeling messages exchanged between    *
 * processes I and J during round K (these messages are enumerated in file   *
 * labels-$J-$I-$K). We then check that it is large enough, by using         *
 * projection (to extract the part of the medium that was indeed useful)     *
 * and a temporal logic formula.                                             *)

%         LABELS=`cat labels-$J-$I-$K | xargs`
%         printf "\n-- Creating medium.bcg to handle communications between processes"
%         printf "\n-- number $J and $I at round $K and verifying that it is large enough\n"

          "medium.bcg" = bag 5 with {$LABELS};

          "tmp.bcg" = generation of
                "$2.bcg" |[ {$LABELS} ]| "medium.bcg";

          "projection.bcg" = "medium.bcg" -|[ {$LABELS} ]|
                             (branching reduction of
                              hide all but {$LABELS} in "tmp.bcg");

          (* Check using temporal logic formulas that the media are large
           * enough to handle all messages; one actually checks that 5
           * consecutive emissions cannot be made on the media restricted
           * using semi-composition *)

          property MEDIUM_OK is
          -- version 1: dataless formula
          "projection.bcg" |= with evaluator 
              ['SEND.*' . 'SEND.*' . 'SEND.*' . 'SEND.*' . 'SEND.*'] false;
          expected TRUE;

          -- version 2: value-passing formula
          "projection.bcg" |= with evaluator
              [ 'SEND.*' { 5 } ] false;
          expected TRUE
          end property;

          (* LABELS are no longer needed in result $2.bcg. Hide and continue *)

          "$2.bcg" = branching reduction of 
                hide {$LABELS} in "tmp.bcg";

%         K=`expr $K + 1`
%       done
%       J=`expr $J + 1`
%     done
%   done

% }

(*---------------------------------------------------------------------------*
 * Function COMPOSE_ROUNDS generates the LTS modeling the execution of $1    *
 * rounds of the protocol, by composing rounds. The LTS of one round is      *
 * given in BCG file $2.bcg, and result is stored in file $3.bcg.            *
 *---------------------------------------------------------------------------*)

% COMPOSE_ROUNDS () {

    "$3.bcg" = "$2.bcg";

%   ROUND=2
%   while [ $ROUND -le $1 ]
%   do
%     printf "\nRound $ROUND\n"
%     PREV_ROUND=`expr $ROUND - 1`

      "$3.bcg" = strong reduction of
            "$3.bcg" 
            |[ "OUTPUT_${PREV_ROUND}" ]|
            rename
              "INPUT" -> "OUTPUT_${PREV_ROUND}",
              "OUTPUT_1" -> "OUTPUT_$ROUND"
            in "$2.bcg";

%     ROUND=`expr $ROUND + 1`
%   done

% }

(*---------------------------------------------------------------------------*
 * This is where the script execution starts.                                *
 *---------------------------------------------------------------------------*)

% printf "\n----------------------------------------------------------------"
% printf "\nCompositional generation of the first round of the protocol for"
% printf "\n3 processes using a decomposition into processes and media"
% printf "\n----------------------------------------------------------------\n"

% GENERATE_ROUNDS 1 "1round"

% printf "\n----------------------------------------------------------------"
% printf "\nGeneration of the LTS modeling 2 rounds for 3 processes using"
% printf "\nthe same method as that used to generate the LTS of one round"
% printf "\n(no decomposition into rounds). This may take much longer"
% printf "\n----------------------------------------------------------------\n"

% GENERATE_ROUNDS 2 "2rounds"

% printf "\n----------------------------------------------------------------"
% printf "\nComputation of the LTS of round 2 from that of round 1"
% printf "\n----------------------------------------------------------------\n"

% COMPOSE_ROUNDS 2 "1round" "2rounds-compositional"

% printf "\n----------------------------------------------------------------"
% printf "\nBranching equivalence checking of LTSs obtained by each method"
% printf "\n----------------------------------------------------------------\n"

"diag.bcg" = branching comparison
      "2rounds.bcg" == "2rounds-compositional.bcg";

% printf "\n----------------------------------------------------------------"
% printf "\nGeneration of LTS modeling $NB_ROUNDS rounds for 3 processes"
% printf "\nusing the second method (round compositionality)"
% printf "\n----------------------------------------------------------------\n"

% COMPOSE_ROUNDS $NB_ROUNDS "1round" "${NB_ROUNDS}rounds"

% printf "\n----------------------------------------------------------------"
% printf "\nVerifying that if a process decides one value, it is not"
% printf "\npossible for another process to decide a different value"
% printf "\n----------------------------------------------------------------\n"

property DECISION is
     -- version 1: dataless property
     "${NB_ROUNDS}rounds.bcg" |= with evaluator
         [true* .
             (("DEC !FALSE" . true* . "DEC !TRUE")
              |
              ("DEC !TRUE" . true* . "DEC !FALSE"))
         ] false;
     expected TRUE;

     -- version 2: value-passing property
     "${NB_ROUNDS}rounds.bcg" |= with evaluator
         (* The occurrence of two different decisions is forbidden. *)
         [ true* . { DEC ?b1:bool } . true* . { DEC ?b2:bool } ] (b1 = b2);
     expected TRUE
end property

(*---------------------------------------------------------------------------*
 * Comparison between the LOTOS and LNT specifications.                      *
 *---------------------------------------------------------------------------*)

% PROCESS="INPUT_VALUES [SEND, RECV, DEC, INPUT, OUTPUT]"

% SVL_RECORD_FOR_CLEAN "lts.bcg" "LOTOS/lts.bcg"

% for PARAMETERS in "(3, 0, 1, 1, 1)" "(3, 0, 2, 1, 2)" "(3, 1, 3, 1, 3)" \
%    "(3, 1, 1, 1, 4)" "(3, 2, 2, 1, 5)" "(3, 2, 3, 1, 6)" \
%    "(3, 0, 1, 1, 7)" "(3, 1, 2, 1, 8)" "(3, 2, 3, 1, 9)"
% do
	"lts.bcg" = generation of "CONSENSUS.lnt":"$PROCESS $PARAMETERS" ;
%	cd LOTOS
	"lts.bcg" = generation of "CONSENSUS.lotos":"$PROCESS $PARAMETERS" ;
%	cd ..
	strong comparison "lts.bcg" == "LOTOS/lts.bcg" ;
% done