-------------------------------------------------------------------------------
--           M U T U A L     E X C L U S I O N     P R O T O C O L S
-------------------------------------------------------------------------------

-- $N is the number of concurrent processes participating in the protocol
-- read optional command-line argument; by default, $N = 2

% if [ $# -eq 0 ]
% then
%	DEFAULT=1
%	N=2
% else
%	DEFAULT=0
%	case "$1" in
%	0 | 1 )
%		echo "error: number of processors must be greater than 1"
%		exit 1
%		;;
%	2 | 3 | 4 | 5 )
%		N=$1
%		shift
%		;;
%	[0-9]* )
%		echo "error: number of processors must be less than 6"
%		# (or provide the corresponding files Architectures/ARCH_*
%		# and Architectures/TYPES_*)
%		exit 1
%		;;
%	* )
%		# $1 is assumed to be a protocol name (1st item of $SPEC_LIST)
%		N=2
%	esac
% fi

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

-- compute the list of process identifiers, i.e., "0 .. ($N-1)"

% MAX_PID=`expr $N - 1`

% PID_LIST=`seq 0 $MAX_PID`

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

-- compute the list of procotols (possibly given on the command line)

% SPEC_LIST="$*"

% if [ "$DEFAULT" = 1 ]
% then

-- here, $SPEC_LIST is empty and $N = 2; select a small subset of protocols
-- to have a demo example that does not take too much time

% SPEC_LIST="anderson dekker dijkstra knuth lamport peterson szymanski"

% elif [ "$SPEC_LIST" = "" ]
% then

-- protocols for any number of processes

% SPEC_LIST="anderson burns_lynch bw_bakery clh dijkstra knuth lamport mcs \
%            peterson peterson_tree szymanski tas ttas trivial"

-- additional protocols for two processes

% if [ $N -eq 2 ]
% then
% SPEC_LIST="$SPEC_LIST dekker kessels_2 knuth_2 peterson_2 \
%            mutex_2b_p1 mutex_2b_p2 mutex_2b_p3 mutex_3b_p1 mutex_3b_p2 \
%            mutex_3b_c_p1_orig mutex_3b_c_p1 mutex_3b_c_p2 mutex_3b_c_p3 \
%            mutex_4b_p1 mutex_4b_p2 mutex_4b_c_p1 mutex_4b_c_p2"
% fi

% fi

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

-- instantiation of the libraries for $N processes

% for MODULE in ARCH_1B ARCH_1Q ARCH_2B ARCH_3B ARCH_3B_Q ARCH_3B_A ARCH_4B ARCH_4B_Q ARCH_5B ARCH_7B ARCH_TREE TYPES
% do
%	$CADP/src/com/cadp_ln Architectures/${MODULE}_$N.lnt $MODULE.lnt
%	SVL_RECORD_FOR_CLEAN "$MODULE.lnt"
% done

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

-- creation of symbolic links to the generic component libraries

% for MODULE in Components/*.lnt
% do
%	$CADP/src/com/cadp_ln $MODULE .
%	SVL_RECORD_FOR_CLEAN `basename $MODULE`
% done

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

-- creation of symbolic links to protocols

% for SPEC in $SPEC_LIST
% do
%	$CADP/src/com/cadp_ln Protocols/$SPEC.lnt $SPEC.lnt
%	SVL_RECORD_FOR_CLEAN "$SPEC.lnt"
% done

-------------------------------------------------------------------------------
-- PHASE 1: definitions for functional verification by model checking
-------------------------------------------------------------------------------

-- creation of a macro library (included by all formulae)

% echo "macro N () = $MAX_PID end_macro" > macro.mcl
% SVL_RECORD_FOR_CLEAN "macro.mcl"

% DEFAULT_MCL_LIBRARIES="macro.mcl"

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

property mutual_exclusion (SPEC)
	"$SPEC ensures mutual exclusion"
is
	"protocol.bcg" |= with evaluator4
		[
		    true* .
		    {CS !"ENTER" ?i:Nat} .
		    (not {CS !"LEAVE" !i})* .
		    {CS !"ENTER" ?j:Nat where j<>i}
		] false;
	expected TRUE;
end property

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

property livelock_free (SPEC)
	"$SPEC is free of livelocks as defined in [Anderson-Kim-Herman-03]"
is
	-- The formula below is too strict, because of the busy waiting cycles
	-- where one process waits while the others do nothing. This is
	-- unrealistic if we assume that the system's scheduler is fair, so
	-- every process is guaranteed to progress.
	"protocol.bcg" |= with evaluator4
		[
		    true* .
		    {NCS ?i:Nat} .
		    (not {?G:String ... !i where (G<>"CS") and (G<>"NCS")})* .
		    {?G:String ... !i where (G<>"CS") and (G<>"NCS")}
		]
		mu X . (< true > true and [ not {CS !"ENTER" ?any} ] X);
	expected FALSE;

	-- The formula below states that after some process Pi has begun its
	-- entry section, then there is no unfair cycle in which every process
	-- executes at least one action but no process enters its critical
	-- section.
	"protocol.bcg" |= with evaluator4
		[
		    true* .
		    {NCS ?i:Nat} .
		    (not {?G:String ... !i where (G<>"CS") and (G<>"NCS")})* .
		    {?G:String ... !i where (G<>"CS") and (G<>"NCS")}
		]
		[
		    for j:Nat from 0 to N do
			(not {CS ...})* . {?G:String ... !j where G<>"CS"}
		    end for
		]-|;
	expected TRUE;
end property

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

property livelock_upon_crash (SPEC)
	"$SPEC livelocks after the crash of a process"
is
	-- Livelock of the protocol after process Pi has crashed while in its
	-- entry section. More precisely, after writing a shared variable by Pi
	-- no process ever enters its critical section, although the processes
	-- other than Pi may execute forever
	"protocol.bcg" |= with evaluator4
		forall i:Nat among {0 ... N} .
		    <
		        true* .
		        {NCS !i} .
		        (not {CS !"ENTER" !i})* .
		        {?any !"WRITE" ... !i} .
		        (not {CS !"ENTER" !i})*
		    >
		    <
			for j:Nat from 0 to N do
			    if j<>i then
				(not {CS ...})* .
			        {?G:String ... !j where G<>"CS"}
			    end if
			end for
		    >@;
	expected TRUE;

	-- specialised formula for the case of two processes
	% if [ $N -eq 2 ]
	% then
	"protocol.bcg" |= with evaluator4
		forall i: Nat among {0 ... 1} .
		    <
		        true* .
		        {NCS !i} .
		        (not {CS !"ENTER" !i})* .
		        {?any !"WRITE" ... !i} .
		        (not {CS !"ENTER" !i})*
		    >
		    < {?G:String ... ?j:Nat where (i<>j) and (G<>"CS")} >@;
	expected TRUE;
	% fi
end property

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

property deadlock_free (SPEC)
	"$SPEC is free of deadlocks"
is
	-- Absence of livelocks (defined misleadingly as "deadlocks" in
	-- [Bar-David-Taubenfeld-03]), which forbids the existence of a cycle
	-- containing at least one instruction executed by each process but no
	-- accesses to the critical sections
	"protocol.bcg" |= with evaluator4
		[ true* ]
		[
		    for i:Nat from 0 to N do
			(not {CS ...})* .
			{?G:String ... !i where G<>"CS"}
		    end for
		]-|;
	expected TRUE;
end property

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

property local_deadlock_free (SPEC)
	"$SPEC is free of local deadlocks"
is
	-- from every state, each process Pi can execute an action
	"protocol.bcg" |= with evaluator4
		[ true* ] (
		    < {MU ...} > true
		    or
		    forall i:Nat among {0 ... N} . < {... !i} > true
		);
	expected TRUE;
end property

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

property starvation_free (SPEC)
	"$SPEC is free of starvation"
is
	-- The formula below is too strict, because of the busy waiting cycles
	-- where one process waits while the others do nothing. This is
	-- unrealistic if we assume that the system's scheduler is fair, so
	-- every process is guaranteed to progress.
	"protocol.bcg" |= with evaluator4
		[
		    true* .
		    {NCS ?i:Nat} .
		    (not {?G:String ... !i where (G<>"CS") and (G<>"NCS")})* .
		    {?G:String ... !i where (G<>"CS") and (G<>"NCS")}
		]
		mu X . (< true > true and [ not {CS !"ENTER" !i} ] X);
	expected FALSE;

	-- The formula below states that after some process Pi has begun its
	-- entry section, then there is no unfair cycle in which every process
	-- executes at least one action but the demanding process does not
	-- enter its critical section.
	"protocol.bcg" |= with evaluator4
		[
		    true* .
		    {NCS ?i:Nat} .
		    (not {?G:String ... !i where (G<>"CS") and (G<>"NCS")})* .
		    {?G:String ... !i where (G<>"CS") and (G<>"NCS")}
		]
		[
		    for j:Nat from 0 to N do
			(not {CS ... !i})* .
			{?G:String ... !j where (j=i) implies (G<>"CS")}
		    end for
		]-|;
	expected TRUE;

	-- Absence of starvation for process Pi (i in [0..N]) defined as in
	-- [Bar-David-Taubenfeld-03], which forbids the existence of a cycle
	-- containing at least one instruction executed by each process but no
	-- access of process Pi to its critical section
	"protocol.bcg" |= with evaluator4
		[ true* ]
		    forall i:Nat among {0 ... N} .
			[
			    for j:Nat from 0 to N do
				(not { CS ... !i })* .
				{?G:String ... !j where (j=i) implies (G<>"CS")}
			    end for
			]-|;
	expected TRUE;
end property

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

property independent_progress (SPEC)
	"$SPEC satisfies independent progress"
is
	-- The formula below expresses that every time a process Pj has stopped
	-- in its non critical section, all other processes Pi can access their
	-- critical sections. This is the formula used in [Mateescu-Serwe-13].
	"protocol.bcg" |= with evaluator4
		[ true* ]
		    forall j:Nat among {0 ... N} . (
			< {NCS !j} > true
			implies
			[ (not {... !j})* ]
			    forall i:Nat among {0 ... N} . (
				(i<>j)
				implies
				< (not {... !j})* > < {... !i}* . {CS ... !i} >@
			    )
		    );
	expected TRUE;

	-- The formula below generalizes the previous formula. It expresses
	-- that every time some processes Pj have stopped in their non
	-- critical sections, all other processes Pi can freely access their
	-- critical sections.
	"protocol.bcg" |= with evaluator4
		nu X (idle:NatSet:=empty) . (
		    forall i:Nat among { 0 ... N } . (
			(not (i isin idle))
			implies
			< (not {... ?j:Nat where j isin idle})* >
			    < {... !i}* . {CS ... !i} >@
		    )
		    and
		    [ not {... ?j:Nat where j isin idle} ] X (idle)
		    and
		    [ {... ?j:Nat where j isin idle} ] X (remove (j, idle))
		    and
		    forall j:Nat among { 0 ... N } . (
			((not (j isin idle)) and < {NCS !j} > true)
			implies
			X (insert (j, idle))
		    )
		);
	expected TRUE;
end property

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

property local_starvation_free (SPEC, PID)
	"$SPEC: process $PID is free of starvation"
is
	-- The formula below expresses absence of starvation for process $PID
	-- as defined in [Bar-David-Taubenfeld-03], which forbids the existence
	-- of a cycle containing at least one instruction executed by each
	-- process but no access of process $PID to its critical section
	"protocol.bcg" |= with evaluator4
		[ true* ]
		    [
			for j:Nat from 0 to N do
			    (not {CS ... !$PID})* .
			    {?G:String ... !j
			       where (j = $PID) implies (G <> "CS") }
			end for
		    ]-|;
	expected TRUE;
end property

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

property local_independent_progress (SPEC, PID)
	"$SPEC: process $PID can progress independently"
is
	-- Independent progress of process $PID, meaning the existence of
	-- a cycle in which process $PID accesses its critical section each
	-- time another process Pj remains stuck in its non-critical section;
	-- there is no constraint on the behavior of the other processes
	"protocol.bcg" |= with evaluator4
		forall j:Nat among { 0 ... N } .
		(
		    (j <> $PID) implies
		    [ true* ] (
		        < {NCS !j} > true
		        implies
		        <
		            {... ?k:Nat where k <> j}* .
		            {CS !"ENTER" !$PID} .
		            {... ?k:Nat where k <> j}* .
		            {CS !"LEAVE" !$PID}
		        >@
		    )
		);
	expected TRUE;
end property

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

property unbounded_overtaking (SPEC, I, J)
	"$SPEC: unbounded overtaking of process $J by process $I"
is
	-- The formula below expresses unbounded overtaking of process $J by
	-- process $I after process $J has begun its entry section, i.e., it
	-- requests the access to the critical section
	"protocol.bcg" |= with evaluator4
		<
		    true* .
		    {NCS !$J} .
		    (not {?G:String ... !$J
                       where (G <> "CS") and (G <> "NCS")})* .
		    {?G:String ... !$J where (G <> "CS") and (G <> "NCS")}
		>
		<
		    for j:Nat from 0 to N do
		       (not {CS ... !$J})* .
		       {?G:String ... !j where (j = $J) implies (G <> "CS")}
		    end for .
		    (not {CS ?any !$J})* .
		    {CS !"ENTER" !$I}
		>@;
end property

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

property bounded_overtaking (SPEC, I, J, MAX)
	"$SPEC: process $I overtakes process $J at most $MAX times"
is
	-- The formula below expresses that process $I overtakes process $J at
	-- most $MAX times, i.e., the maximal number of times process $I
	-- enters its critical section after process $J has begun its entry
	-- section but did not access its critical section
	"protocol.bcg" |= with evaluator4
		<
		    true* .
		    {NCS !$J} .
		    (not {?G:String ... !$J
                       where (G <> "CS") and (G <> "NCS")})* .
		    {?G:String ... !$J where (G <> "CS") and (G <> "NCS")} .
		    (
			for j:Nat from 0 to N do
			   (not {CS ... !$J})* .
			   {?G:String ... !j
                              where (j = $J) implies (G <> "CS")}
			end for .
			(not {CS ?any !$J})* .
			{CS !"ENTER" !$I}
		    ) { $MAX }
		> true;
end property

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

% VERIFY() {
-- $1: name of the protocol (i.e., $SPEC)

-- global properties

check mutual_exclusion ("$1");
check livelock_free ("$1");
check livelock_upon_crash ("$1");
check deadlock_free ("$1");
check local_deadlock_free ("$1");
check starvation_free ("$1");
check independent_progress ("$1");

-- local properties for a given process

% for PID in $PID_LIST
% do
	check local_starvation_free ("$1", "$PID");
	check local_independent_progress ("$1", "$PID");
% done

-- overtaking (for pairs of processes)

% for I in $PID_LIST
% do
%	for J in $PID_LIST
%	do
%		if [ "$J" = "$I" ]
%		then
%			continue
%		fi
		check unbounded_overtaking ("$1", "$I", "$J");
%		for BOUND in 1 2 4
%		do
			check bounded_overtaking ("$1", "$I", "$J", "$BOUND");
%		done
%	done
% done

% }

-------------------------------------------------------------------------------
-- PHASE 2.0: common definitions for performance evaluation
-------------------------------------------------------------------------------

-- generation of the hiding file used by all experiments

% cat > "hide.hid" << EOF
%hide all but
%"MU.*"
%EOF

% SVL_RECORD_FOR_SWEEP "hide.hid"

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

% INITIALIZE_THROUGHPUTS() {
-- $1 = throughput file

% printf "%s" '# "spec" "ratio"' > $1
% for PID in $PID_LIST
% do
%	printf " \"CS_%u\"" $PID >> $1
% done
% echo "" >> $1

% }

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

% THROUGHPUT1="experiment_1.thr"
% INITIALIZE_THROUGHPUTS $THROUGHPUT1

% THROUGHPUT2="experiment_2.thr"
% INITIALIZE_THROUGHPUTS $THROUGHPUT2

% THROUGHPUT3="experiment_3.thr"
% echo '# "ratio" "CS_0" "CS_1"' > $THROUGHPUT3

% SVL_RECORD_FOR_CLEAN "$THROUGHPUT1" "$THROUGHPUT2" "$THROUGHPUT3"

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

-- compute the product of two floating-point numbers, removing trailing zeros

% MUL() {
% echo "$1 * $2" | bc -l | sed -e 's/\.[0]*$//'
% }

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

-- compute the quotient of two floating-point numbers, removing trailing zeros

% DIV() {
% echo "$1 / $2" | bc -l | sed -e 's/\.[0]*$//'
% }

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

-- given two rates $1 and $2, compute 1 / ( 1/$1 + 1/$2 )

% SUM() {
% DIV "($1 * $2)" "($1 + $2)"
% }

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

-- memory access rates to the shared memory

% READ_RATE=3000
% WRITE_RATE=2000
% FETCH_RATE=`SUM $READ_RATE $WRITE_RATE`
% COMPARE_RATE=$FETCH_RATE
% READ_AND_INCREMENT_RATE=$FETCH_RATE

-- memory access rates to local caches

% READ_LOCAL_RATE=`MUL $READ_RATE 50`
% READ_REMOTE_RATE=`SUM $WRITE_RATE $READ_RATE`
% WRITE_LOCAL_RATE=`MUL $READ_LOCAL_RATE .9`
% WRITE_REMOTE_RATE=$WRITE_RATE
% FETCH_LOCAL_RATE=`SUM $READ_LOCAL_RATE $WRITE_LOCAL_RATE`
% FETCH_REMOTE_RATE=`SUM $READ_REMOTE_RATE $WRITE_REMOTE_RATE`

% COMPARE_LOCAL_RATE=$FETCH_LOCAL_RATE
% COMPARE_REMOTE_RATE=$FETCH_REMOTE_RATE

% READ_AND_INCREMENT_LOCAL_RATE=$FETCH_LOCAL_RATE
% READ_AND_INCREMENT_REMOTE_RATE=$FETCH_REMOTE_RATE

-- similar to [Yang-Anderson-95] and [David-Guerraoui-Trigonakis-13], a
-- critical section roughly corresponds to the incrementation of a counter,
-- i.e., a read and a write
-- note: in [Mateescu-Serwe-10], the following fixed rate was used
-- CS_RATE=100

% CS_RATE=`SUM $WRITE_RATE $READ_RATE`

-- the value of $PROB must be such that $N * $PROB is less or equal than 1
-- (otherwise bcg_steady will complain) ; if $N * $PROB is strictly less than
-- 1, bcg_steady will automatically perform the required normalization

% PROB=0.005

-- default options for steady-state simulation

% CUNCTATOR_OPTIONS="-rate -rng 2 -scheduler 2 -depth 1000000 -hide -total hide.hid"

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

% COMPUTE_THROUGHPUTS() {
-- $1: 1 iff "imc.bcg" has been generated (i.e., $EXHAUSTIVE)
-- $2: throughput file (with ".thr" extension) -- for bcg_steady only
-- $3: rename file (without ".ren" extension)

% if [ $1 = 1 ]
% then
	-- steady-state analysis using BCG_STEADY

	"ctmc.bcg" =
		total rename "i" -> "prob $PROB" in
		total rename using "$3.ren" in
		"imc.bcg" ;

%	SVL_ECHO "bcg_steady (ratio: $RATIO)"
%	bcg_steady -thr -append $2 ctmc.bcg spec=$SPEC ratio=$RATIO
%	SVL_RECORD_FOR_SWEEP "ctmc.bcg"
% else
	-- simulation using CUNCTATOR

	-- use several seeds for the random number generator to get precision
%	for SEED in 1 42 911
%	do
%		SVL_ECHO "./cunctator (ratio: $RATIO, seed: $SEED)"
		-- the "2>>" redirection is meant for the $CADP_TIME command
%		$CADP_TIME ./cunctator -seed $SEED $CUNCTATOR_OPTIONS -rename -total $3.ren -thr -append $2 spec=$SPEC ratio=$RATIO 2>> $SVL_LOG_FILE
%	done
% fi

% }

-------------------------------------------------------------------------------
-- PHASE 2.1: definitions for performance evaluation: experiment 1
-- compute throughputs without caches as in [Mateescu-Serwe-10]
-------------------------------------------------------------------------------

% EVALUATE_1() {
-- $1: name of the protocol (i.e., $SPEC)
-- $2: 1 iff "imc.bcg" has been generated (i.e., $EXHAUSTIVE)

% echo "\"$1\"" >> $THROUGHPUT1

% for RATIO in 0.25 0.5 1 2 4 8 16 32
% do
%	NCS_RATE=`DIV $CS_RATE $RATIO`

	-- generate renaming for Markov delays associated to actions

%	cat > "rename1.ren" << EOF
%rename
%"MU !READ.*"                 -> "rate $READ_RATE"
%"MU !WRITE.*"                -> "rate $WRITE_RATE"
%"MU !FETCH_AND_STORE.*"      -> "rate $FETCH_RATE"
%"MU !COMPARE_AND_SWAP.*"     -> "rate $COMPARE_RATE"
%"MU !READ_AND_INCREMENT.*"   -> "rate $READ_AND_INCREMENT_RATE"
%"MU !WORK.*"                 -> "rate $NCS_RATE"
%"MU !ENTER !\([0-9][0-9]*\)" -> "CS_\1; rate $CS_RATE"
%EOF

%	SVL_SHOW_FILE_IN_LOG "rename1.ren"
%	COMPUTE_THROUGHPUTS $2 $THROUGHPUT1 "rename1"
% done

% echo "" >> $THROUGHPUT1
% echo "" >> $THROUGHPUT1

% SVL_RECORD_FOR_SWEEP "rename1.ren"

% }

-------------------------------------------------------------------------------
-- PHASE 2.2: definitions for performance evaluation: experiment 2
-- compute throughputs with caching
-------------------------------------------------------------------------------

% EVALUATE_2() {
-- $1: name of the protocol (i.e., $SPEC)
-- $2: 1 iff "imc.bcg" has been generated (i.e., $EXHAUSTIVE)

-- similar to [Anderson-90], we consider that the non-critical section is,
-- on average, five times as long as the critical section

% RATIO=5
% NCS_RATE=`DIV $CS_RATE $RATIO`

-- generate renaming for Markov delays associated to actions

% cat > "rename2.ren" << EOF
%rename
%"MU !READ_FROM_LOCAL.*"           -> "rate $READ_LOCAL_RATE"
%"MU !READ_FROM_MEMORY.*"          -> "rate $READ_RATE"
%"MU !READ_FROM_REMOTE.*"          -> "rate $READ_REMOTE_RATE"
%"MU !WRITE_TO_LOCAL.*"            -> "rate $WRITE_LOCAL_RATE"
%"MU !WRITE_AND_FETCH.*"           -> "rate $WRITE_RATE"
%"MU !WRITE_AND_INVALIDATE.*"      -> "rate $WRITE_REMOTE_RATE"
%"MU !FETCH_AND_STORE_LOCAL.*"     -> "rate $FETCH_LOCAL_RATE"
%"MU !FETCH_AND_STORE_SHARED.*"    -> "rate $FETCH_RATE"
%"MU !FETCH_AND_STORE_GLOBAL.*"    -> "rate $FETCH_REMOTE_RATE"
%"MU !COMPARE_AND_SWAP_LOCAL.*"    -> "rate $COMPARE_LOCAL_RATE"
%"MU !COMPARE_AND_SWAP_SHARED.*"   -> "rate $COMPARE_RATE"
%"MU !COMPARE_AND_SWAP_GLOBAL.*"   -> "rate $COMPARE_REMOTE_RATE"
%"MU !READ_AND_INCREMENT_LOCAL.*"  -> "rate $READ_AND_INCREMENT_LOCAL_RATE"
%"MU !READ_AND_INCREMENT_SHARED.*" -> "rate $READ_AND_INCREMENT_RATE"
%"MU !READ_AND_INCREMENT_GLOBAL.*" -> "rate $READ_AND_INCREMENT_REMOTE_RATE"
%"MU !WORK.*"                      -> "rate $NCS_RATE"
%"MU !ENTER !\([0-9][0-9]*\)"      -> "CS_\1; rate $CS_RATE"
%EOF

% SVL_SHOW_FILE_IN_LOG "rename2.ren"

% COMPUTE_THROUGHPUTS $2 $THROUGHPUT2 "rename2"

% }

-------------------------------------------------------------------------------
-- PHASE 2.3: definitions for performance evaluation: experiment 3
-- only for two processes; vary ratio "rate_ncs_0/rate_ncs_1" (without caches)
-------------------------------------------------------------------------------

% EVALUATE_3() {
-- $1: name of the protocol (i.e., $SPEC)

% echo "\"$1\"" >> $THROUGHPUT3

-- preliminary renaming common to all values of ratio

"renamed.bcg" =
	total rename
		"i"                        -> "prob ${PROB}",
		"MU !READ.*"               -> "rate $READ_RATE",
		"MU !WRITE.*"              -> "rate $WRITE_RATE",
		"MU !FETCH_AND_STORE.*"    -> "rate $FETCH_RATE",
		"MU !COMPARE_AND_SWAP.*"   -> "rate $COMPARE_RATE",
		"MU !READ_AND_INCREMENT.*" -> "rate $READ_AND_INCREMENT_RATE",
		"MU !ENTER !0"             -> "CS_0; rate $CS_RATE",
		"MU !ENTER !1"             -> "CS_1; rate $CS_RATE"
	in "imc.bcg" ;

% SVL_RECORD_FOR_SWEEP "renamed.bcg"

% NCS_RATE=50.0

-- process 0 slower than process 1: ratio < 1

% for RATIO in 16 8 4 2
% do
%	OTHER_NCS_RATE=`DIV $NCS_RATE $RATIO`

	"ctmc.bcg" =
		total rename
			"MU !WORK !0" -> "rate $OTHER_NCS_RATE",
			"MU !WORK !1" -> "rate $NCS_RATE"
		in "renamed.bcg" ;

%	SVL_ECHO "bcg_steady (ratio: $RATIO)"

%	bcg_steady -thr -append $THROUGHPUT3 ctmc.bcg ratio=`DIV 1 $RATIO`
% done

-- process 0 and process 1 equally fast: ratio = 1

"ctmc.bcg" =
	total rename "MU !WORK.*" -> "rate $NCS_RATE"
	in "renamed.bcg" ;

% SVL_ECHO "bcg_steady (ratio: $RATIO)"

% bcg_steady -thr -append $THROUGHPUT3 ctmc.bcg ratio=1

-- process 0 faster than process 1: ratio > 1

% for RATIO in 2 4 8 16
% do
%	OTHER_NCS_RATE=`DIV $NCS_RATE $RATIO`

	"ctmc.bcg" =
		total rename
			"MU !WORK !0" -> "rate $NCS_RATE",
			"MU !WORK !1" -> "rate $OTHER_NCS_RATE"
		in "renamed.bcg" ;

%	SVL_ECHO "bcg_steady (ratio: $RATIO)"

%	bcg_steady -thr -append $THROUGHPUT3 ctmc.bcg ratio=$RATIO
% done

% echo "" >> $THROUGHPUT3
% echo "" >> $THROUGHPUT3

% }

-------------------------------------------------------------------------------
-- PHASE 3: running model-checking verification and performance evaluation
-------------------------------------------------------------------------------

% if [ $N -lt 4 ]
% then
	-- generate state spaces exhaustively only for N < 4
%	EXHAUSTIVE=1
% else
%	EXHAUSTIVE=0
% fi

% for SPEC in $SPEC_LIST
% do
%	if [ $EXHAUSTIVE = 1 ]
%	then
%		SVL_ECHO "*** state-space generation and minimization for $SPEC protocol"
		"protocol.bcg" = reduction of "$SPEC.lnt":PROTOCOL ;

%		SVL_ECHO "*** model-checking verification of $SPEC protocol"
%		VERIFY $SPEC

%		SVL_ECHO "*** IMC compositional generation for $SPEC protocol"
		"imc.bcg" =
			total hide using "hide.hid" in
				generation of
				"protocol.bcg"
				|[NCS, CS, A, B, C, D]|
				(
					"$SPEC.lnt":L
					-|[NCS, CS, A, B, C, D]|
					"protocol.bcg"
				) ;
		-- "imc.bcg" must not be reduced using strong bisimulation
%	else
%		SVL_ECHO "*** simulator generation for $SPEC protocol"
		-- generation of the CUNCTATOR executable for simulation
%		lnt.open $SPEC.lnt cunctator -version > /dev/null 2>&1
%	fi

%	if [ $SPEC = "bw_bakery" -a $N -eq 3 ]
%	then
		-- for N == 3, steady-state analysis of the black-white bakery
		-- protocol requires about 21 hours; for N > 3, the problem
		-- vanishes as CUNCTATOR is used instead of BCG_STEADY
%		continue
%	fi

%	SVL_ECHO "*** performance evaluation 1 (without caching) of $SPEC protocol"
%	EVALUATE_1 $SPEC $EXHAUSTIVE

%	SVL_ECHO "*** performance evaluation 2 (with caching) of $SPEC protocol"
%	EVALUATE_2 $SPEC $EXHAUSTIVE

%	if [ $N -eq 2 ]
%	then
%		SVL_ECHO "*** performance evaluation 3 (varying relative speeds) of $SPEC protocol"
%		EVALUATE_3 $SPEC
%	fi

%	SVL_RECORD_FOR_SWEEP "protocol.bcg" "imc.bcg"
%	SVL_RECORD_FOR_SWEEP "$SPEC.c" "$SPEC.h" "$SPEC.o"
%	SVL_RECORD_FOR_SWEEP "cunctator" "evaluator4" "generator" "generator.o"
% done


-------------------------------------------------------------------------------
-- PHASE 4: drawing diagrams by calling Gnuplot
-------------------------------------------------------------------------------

-- run Gnuplot to generate mutex.pdf
% gnuplot mutex.plot

-- display mutex.pdf
% "$CADP"/src/com/cadp_pdf mutex.pdf

% SVL_RECORD_FOR_CLEAN "mutex.pdf"