-------------------------------------------------------------------------------
--           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
%		;;
%	[6-9] | [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: functional verification / model checking
-------------------------------------------------------------------------------

property mutual_exclusion (SPEC)
	"$SPEC ensures mutual exclusion"
is
	"${SPEC}_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.
	"${SPEC}_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.
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[
		    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_free_upon_crash (SPEC)
	"$SPEC is free of livelocks, even after the crash of a process"
is
	-- Livelock of the protocol after process Pi has crashed during its
	-- entry section, i.e., after Pi has crashed after writing a shared
	-- variable during its entry section, the other processes may execute
	-- forever, none of them accessing its critical section
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		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
	"${SPEC}_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 as 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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[ 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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[ 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.
	"${SPEC}_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.
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[
		    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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[ 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].
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[ 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.
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		[ 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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		<
		    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
	"${SPEC}_protocol.bcg" |= with evaluator4
		macro N () = $MAX_PID end_macro
		<
		    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() {
-- argument 1: name of the protocol

% SPEC=$1

-- LTS generation and minimization for $SPEC.lnt

"${SPEC}_protocol.bcg" = reduction of "$SPEC.lnt":PROTOCOL ;

% if [ ! -f "${SPEC}_protocol.bcg" ]
% then
%	SVL_ECHO "absence of \"${SPEC}_protocol.bcg\": skipping model-checking"
%	return
% fi

-- global properties

check mutual_exclusion ("$SPEC");
check livelock_free ("$SPEC");
check livelock_free_upon_crash ("$SPEC");
check deadlock_free ("$SPEC");
check local_deadlock_free ("$SPEC");
check starvation_free ("$SPEC");
check independent_progress ("$SPEC");

-- local properties for a given process

% for PID in $PID_LIST
% do
	check local_starvation_free ("$SPEC", "$PID");
	check local_independent_progress ("$SPEC", "$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 ("$SPEC", "$I", "$J");
%		for BOUND in 1 2 4
%		do
			check bounded_overtaking ("$SPEC", "$I", "$J", "$BOUND");
%		done
%	done
% done

% }

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

-- verifying all protocols of $SPEC_LIST, only if $N <= 4
-- for N = 4, LTS generation and model checking require 16 GB of RAM

% if [ $N -lt 4 -o \( $N -eq 4 -a `cadp_memory -physical` -lt 17179869184 \) ]
% then
%	for SPEC in $SPEC_LIST
%	do
%		SVL_ECHO "*** model-checking verification of $SPEC protocol" 
%		VERIFY $SPEC
%	done
% fi

% SVL_RECORD_FOR_SWEEP "generator" "generator.o" "evaluator4"

-------------------------------------------------------------------------------
-- PHASE 2: 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"

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

% for SPEC in $SPEC_LIST
% do

% if [ $N -lt 4 ]
% then
	-- compositional generation of the IMC in the BCG format
	-- for N < 4, generate the IMC and use BCG_STEADY
	-- note: these IMC must not be reduced by standard strong bisimulation
	"${SPEC}_hidden.bcg" = 
		total hide using "hide.hid" in
			generation of
			"${SPEC}_protocol.bcg"
			|[NCS, CS, A, B, C, D]|
			(
				"$SPEC.lnt":L
				-|[NCS, CS, A, B, C, D]|
				"${SPEC}_protocol.bcg"
			) ;
%	SVL_RECORD_FOR_SWEEP "${SPEC}_hidden.bcg"
% else
	-- generation of the CUNCTATOR executable for simulation
%	SVL_ECHO "compiling $SPEC"
%	lnt.open $SPEC.lnt cunctator -version > /dev/null 2>&1
%	mv cunctator ${SPEC}_cunctator
%	SVL_RECORD_FOR_SWEEP "$SPEC.c" "${SPEC}.h" "$SPEC.o"
%	SVL_RECORD_FOR_CLEAN "${SPEC}_cunctator"
% fi

% done

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

-- 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 = experiment number (1 or 2)
-- $2 = throughput file (for bcg_steady only)

% if [ $N -lt 4 ]
% then
	-- steady-state analysis using BCG_STEADY

	"${SPEC}_ctmc.bcg" =
		total rename "i" -> "prob $PROB" in
		total rename using "${SPEC}_$1.ren" in
		"${SPEC}_hidden.bcg" ;

%	SVL_ECHO "bcg_steady ${SPEC}_ctmc.bcg"

%	bcg_steady -thr -append $2 ${SPEC}_ctmc.bcg spec=$SPEC ratio=$RATIO

%	SVL_RECORD_FOR_SWEEP "${SPEC}_ctmc.bcg" "${SPEC}_ctmc@1.o"
% else
	-- simulation using CUNCTATOR

%	for SEED in 1 42 911
%	do
%		SVL_ECHO "./${SPEC}_cunctator (ratio: $RATIO, seed: $SEED)"
%		$CADP_TIME ./${SPEC}_cunctator -seed $SEED $CUNCTATOR_OPTIONS -rename -total ${SPEC}_$1.ren > ${SPEC}_$1_${RATIO}_$SEED.cun 2>> $SVL_LOG_FILE

%		LINE="$SPEC $RATIO"
%		for PID in $PID_LIST
%		do
%			LINE="$LINE `grep CS_$PID ${SPEC}_$1_${RATIO}_$SEED.cun | sed 's/.*://'`"
%		done
%		echo "$LINE" >> $2

%		SVL_RECORD_FOR_CLEAN "${SPEC}_$1_${RATIO}_$SEED.cun"
%	done
% fi

% }

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

% EVALUATE_1() {

% SPEC=$1

% echo "\"$SPEC\"" >> $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 > ${SPEC}_1.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 "${SPEC}_1.ren"
%	COMPUTE_THROUGHPUTS 1 $THROUGHPUT1
% done

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

% SVL_RECORD_FOR_SWEEP "${SPEC}_1.ren"
% SVL_RECORD_FOR_SWEEP "${SPEC}_ctmc.bcg" "${SPEC}_ctmc@1.o"

% }

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

% SVL_ECHO "Evaluate performance without caching"

% THROUGHPUT1="experiment_1.thr"
% if [ $N -lt 4 ]
% then
	-- initialize $THROUGHPUT1 file for BCG_STEADY -append
%	echo '# "spec" "ratio" "CS_0" "CS_1" "CS_2"' > $THROUGHPUT1
% fi
% SVL_RECORD_FOR_CLEAN "$THROUGHPUT1"

% for SPEC in $SPEC_LIST
% do
%	if [ $N -eq 3 -a $SPEC = "bw_bakery" ]
%	then
		-- for N == 3, steady-state analysis of the black-white bakery
		-- protocol requires about 21 hours; for N > 3, the problem
		-- vanishes as one is using CUNCTATOR instead of BCG_STEADY
%		SVL_ECHO "skipping black-white bakery protocol"
%	fi
%	EVALUATE_1 $SPEC
% done

-------------------------------------------------------------------------------
-- PHASE 4: performance evaluation experiment 2
-- compute throughputs with caching
-------------------------------------------------------------------------------

% EVALUATE_2() {

-- 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 > ${SPEC}_2.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 "${SPEC}_2.ren"

% COMPUTE_THROUGHPUTS 2 $THROUGHPUT2

% SVL_RECORD_FOR_SWEEP "${SPEC}_2.ren"

% }

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

% SVL_ECHO "Evaluate performance without caching"

% THROUGHPUT2="experiment_2.thr"
% if [ $N -lt 4 ]
% then
	-- initialize ${SPEC}_2.thr file for BCG_STEADY -append
%	echo '# "spec" "ratio" "CS_0" "CS_1" "CS_2"' > $THROUGHPUT2
% fi
% SVL_RECORD_FOR_CLEAN $THROUGHPUT2

% for SPEC in $SPEC_LIST
% do
%	if [ $N -eq 3 -a $SPEC = "bw_bakery" ]
%	then
		-- for N == 3, steady-state analysis of the black-white bakery
		-- protocol requires about 21 hours; for N > 3, the problem
		-- vanishes as one is using CUNCTATOR instead of BCG_STEADY
%		SVL_ECHO "skipping black-white bakery protocol"
%	fi
%	EVALUATE_2 $SPEC
% done

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

% EVALUATE_3() {

% SPEC=$1

% echo "0	    \"$SPEC\"" >> $THROUGHPUT3

-- preliminary renaming common to all values of ratio

"${SPEC}_renamed.bcg" =
	total rename "i" -> "prob ${PROB}" in
	total 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 !ENTER !0"             -> "CS_0; rate $CS_RATE",
		"MU !ENTER !1"             -> "CS_1; rate $CS_RATE"
	in "${SPEC}_hidden.bcg" ;

% SVL_RECORD_FOR_SWEEP "${SPEC}_renamed.bcg" "${SPEC}_renamed@1.o"

% 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`

	"${SPEC}_ctmc.bcg" =
		total rename
			"MU !WORK !0" -> "rate $OTHER_NCS_RATE",
			"MU !WORK !1" -> "rate $NCS_RATE"
		in "${SPEC}_renamed.bcg" ;

%	SVL_ECHO "bcg_steady ${SPEC}_ctmc.bcg"

%	bcg_steady -thr -append $THROUGHPUT3 ${SPEC}_ctmc.bcg ratio=`DIV 1 $RATIO`
% done

% SVL_RECORD_FOR_SWEEP "${SPEC}_ctmc.bcg" "${SPEC}_ctmc@1.o"

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

"${SPEC}_ctmc.bcg" =
	total rename "MU !WORK.*" -> "rate $NCS_RATE"
	in "${SPEC}_renamed.bcg" ;

% SVL_ECHO "bcg_steady ${SPEC}_ctmc.bcg"

% bcg_steady -thr -append $THROUGHPUT3 ${SPEC}_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`

	"${SPEC}_ctmc.bcg" =
		total rename
			"MU !WORK !0" -> "rate $NCS_RATE",
			"MU !WORK !1" -> "rate $OTHER_NCS_RATE"
		in "${SPEC}_renamed.bcg" ;

%	SVL_ECHO "bcg_steady ${SPEC}_ctmc.bcg"

%	bcg_steady -thr -append $THROUGHPUT3 ${SPEC}_ctmc.bcg ratio=$RATIO
% done

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

% }

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

% THROUGHPUT3="experiment_3.thr"
% if [ $N -eq 2 ]
% then
	-- initialize throughput files for BCG_STEADY -append
%	echo '# "ratio" "CS_0" "CS_1"' > $THROUGHPUT3
%	SVL_RECORD_FOR_CLEAN "$THROUGHPUT3"

%	SVL_ECHO "Evaluate performance varying relative speed of processes"

%	for SPEC in $SPEC_LIST
%	do
%		EVALUATE_3 $SPEC
%	done
% fi

-------------------------------------------------------------------------------
-- PHASE 6: 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"