Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

export BK_INPUT=CSRepetitions-PT-07
export BK_EXAMINATION=CTLPlaceComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1659
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/CSRepetitions-PT-07
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is CSRepetitions-PT-07, examination is CTLPlaceComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for CSRepetitions/07 (P/T)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

execution on node 3: quadhexa-2.u-paris10.fr (runId=136933848700107_n_3)
=====================================================================
runnning marcie on CSRepetitions-PT-07 (CTLPlaceComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is CSRepetitions-PT-07, examination is CTLPlaceComparison
=====================================================================

--------------------
content from stdout:

START 1369362712

Marcie rev. 1103M (build: rohrch on 2013-02-17)
A model checker for Generalized Stochastic Petri nets

authors: Alex Tovchigrechko (IDD package and CTL model checking)

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

called as: marcie --net-file=model.pnml --mem=4 --mcc-file=CTLPlaceComparison.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 498 NrTr: 833)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369362712

--------------------
content from stderr:

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok

mcc/mcc_parse.cc:759: Exception: parse error ctl p_1850_placecomparison_eq_x: E F E (X (true & (|marking(Client_Sending_22)|!=|marking(RequestBuffer_22)|) & (|marking(Client_Sending_23)|!=|marking(RequestBuffer_23)|) & (|marking(Client_Sending_17)|!=|marking(RequestBuffer_17)|) & (|marking(Client_Sending_25)|!=|marking(RequestBuffer_25)|) & (|marking(Client_Sending_29)|!=|marking(RequestBuffer_29)|) & (|marking(Client_Sending_2)|!=|marking(RequestBuffer_2)|) & (|marking(Client_Sending_12)|!=|marking(RequestBuffer_12)|) & (|marking(Client_Sending_38)|!=|marking(RequestBuffer_38)|) & (|marking(Client_Sending_48)|!=|marking(RequestBuffer_48)|) & (|marking(Client_Sending_42)|!=|marking(RequestBuffer_42)|) & (|marking(Client_Sending_7)|!=|marking(RequestBuffer_7)|) & (|marking(Client_Sending_32)|!=|marking(RequestBuffer_32)|) & (|marking(Client_Sending_35)|!=|marking(RequestBuffer_35)|) & (|marking(Client_Sending_49)|!=|marking(RequestBuffer_49)|) & (|marking(Client_Sending_44)|!=|marking(RequestBuffer_44)|) & (|marking(Client_Sending_30)|!=|marking(RequestBuffer_30)|) & (|marking(Client_Sending_39)|!=|marking(RequestBuffer_39)|) & (|marking(Client_Sending_26)|!=|marking(RequestBuffer_26)|) & (|marking(Client_Sending_33)|!=|marking(RequestBuffer_33)|) & (|marking(Client_Sending_10)|!=|marking(RequestBuffer_10)|) & (|marking(Client_Sending_14)|!=|marking(RequestBuffer_14)|) & (|marking(Client_Sending_41)|!=|marking(RequestBuffer_41)|) & (|marking(Client_Sending_3)|!=|marking(RequestBuffer_3)|) & (|marking(Client_Sending_18)|!=|marking(RequestBuffer_18)|) & (|marking(Client_Sending_21)|!=|marking(RequestBuffer_21)|) & (|marking(Client_Sending_45)|!=|marking(RequestBuffer_45)|) & (|marking(Client_Sending_20)|!=|marking(RequestBuffer_20)|) & (|marking(Client_Sending_43)|!=|marking(RequestBuffer_43)|) & (|marking(Client_Sending_16)|!=|marking(RequestBuffer_16)|) & (|marking(Client_Sending_15)|!=|marking(RequestBuffer_15)|) & (|marking(Client_Sending_37)|!=|marking(RequestBuffer_37)|) & (|marking(Client_Sending_28)|!=|marking(RequestBuffer_28)|) & (|marking(Client_Sending_6)|!=|marking(RequestBuffer_6)|) & (|marking(Client_Sending_27)|!=|marking(RequestBuffer_27)|) & (|marking(Client_Sending_47)|!=|marking(RequestBuffer_47)|) & (|marking(Client_Sending_9)|!=|marking(RequestBuffer_9)|) & (|marking(Client_Sending_46)|!=|marking(RequestBuffer_46)|) & (|marking(Client_Sending_13)|!=|marking(RequestBuffer_13)|) & (|marking(Client_Sending_11)|!=|marking(RequestBuffer_11)|) & (|marking(Client_Sending_8)|!=|marking(RequestBuffer_8)|) & (|marking(Client_Sending_19)|!=|marking(RequestBuffer_19)|) & (|marking(Client_Sending_34)|!=|marking(RequestBuffer_34)|) & (|marking(Client_Sending_24)|!=|marking(RequestBuffer_24)|) & (|marking(Client_Sending_31)|!=|marking(RequestBuffer_31)|) & (|marking(Client_Sending_1)|!=|marking(RequestBuffer_1)|) & (|marking(Client_Sending_36)|!=|marking(RequestBuffer_36)|) & (|marking(Client_Sending_4)|!=|marking(RequestBuffer_4)|) & (|marking(Client_Sending_5)|!=|marking(RequestBuffer_5)|) & (|marking(Client_Sending_40)|!=|marking(RequestBuffer_40)|)) U !(true & (|marking(Client_Waiting_25)|!=|marking(Client_Sending_25)|) & (|marking(Client_Waiting_26)|!=|marking(Client_Sending_26)|) & (|marking(Client_Waiting_38)|!=|marking(Client_Sending_38)|) & (|marking(Client_Waiting_8)|!=|marking(Client_Sending_8)|) & (|marking(Client_Waiting_48)|!=|marking(Client_Sending_48)|) & (|marking(Client_Waiting_23)|!=|marking(Client_Sending_23)|) & (|marking(Client_Waiting_37)|!=|marking(Client_Sending_37)|) & (|marking(Client_Waiting_4)|!=|marking(Client_Sending_4)|) & (|marking(Client_Waiting_36)|!=|marking(Client_Sending_36)|) & (|marking(Client_Waiting_14)|!=|marking(Client_Sending_14)|) & (|marking(Client_Waiting_20)|!=|marking(Client_Sending_20)|) & (|marking(Client_Waiting_18)|!=|marking(Client_Sending_18)|) & (|marking(Client_Waiting_17)|!=|marking(Client_Sending_17)|) & (|marking(Client_Waiting_11)|!=|marking(Client_Sending_11)|) & (|marking(Client_Waiting_21)|!=|marking(Client_Sending_21)|) & (|marking(Client_Waiting_44)|!=|marking(Client_Sending_44)|) & (|marking(Client_Waiting_45)|!=|marking(Client_Sending_45)|) & (|marking(Client_Waiting_40)|!=|marking(Client_Sending_40)|) & (|marking(Client_Waiting_43)|!=|marking(Client_Sending_43)|) & (|marking(Client_Waiting_41)|!=|marking(Client_Sending_41)|) & (|marking(Client_Waiting_13)|!=|marking(Client_Sending_13)|) & (|marking(Client_Waiting_9)|!=|marking(Client_Sending_9)|) & (|marking(Client_Waiting_3)|!=|marking(Client_Sending_3)|) & (|marking(Client_Waiting_27)|!=|marking(Client_Sending_27)|) & (|marking(Client_Waiting_2)|!=|marking(Client_Sending_2)|) & (|marking(Client_Waiting_19)|!=|marking(Client_Sending_19)|) & (|marking(Client_Waiting_22)|!=|marking(Client_Sending_22)|) & (|marking(Client_Waiting_28)|!=|marking(Client_Sending_28)|) & (|marking(Client_Waiting_6)|!=|marking(Client_Sending_6)|) & (|marking(Client_Waiting_16)|!=|marking(Client_Sending_16)|) & (|marking(Client_Waiting_7)|!=|marking(Client_Sending_7)|) & (|marking(Client_Waiting_49)|!=|marking(Client_Sending_49)|) & (|marking(Client_Waiting_35)|!=|marking(Client_Sending_35)|) & (|marking(Client_Waiting_24)|!=|marking(Client_Sending_24)|) & (|marking(Client_Waiting_5)|!=|marking(Client_Sending_5)|) & (|marking(Client_Waiting_32)|!=|marking(Client_Sending_32)|) & (|marking(Client_Waiting_15)|!=|marking(Client_Sending_15)|) & (|marking(Client_Waiting_1)|!=|marking(Client_Sending_1)|) & (|marking(Client_Waiting_31)|!=|marking(Client_Sending_31)|) & (|marking(Client_Waiting_10)|!=|marking(Client_Sending_10)|) & (|marking(Client_Waiting_39)|!=|marking(Client_Sending_39)|) & (|marking(Client_Waiting_47)|!=|marking(Client_Sending_47)|) & (|marking(Client_Waiting_46)|!=|marking(Client_Sending_46)|) & (|marking(Client_Waiting_33)|!=|marking(Client_Sending_33)|) & (|marking(Client_Waiting_29)|!=|marking(Client_Sending_29)|) & (|marking(Client_Waiting_12)|!=|marking(Client_Sending_12)|) & (|marking(Client_Waiting_42)|!=|marking(Client_Sending_42)|) & (|marking(Client_Waiting_34)|!=|marking(Client_Sending_34)|) & (|marking(Client_Waiting_30)|!=|marking(Client_Sending_30)|)))
ctl p_1851_placecomparison_full_and: A G ((true & (|marking(Client_Sending_22)|=|marking(RequestBuffer_22)|) & (|marking(Client_Sending_23)|=|marking(RequestBuffer_23)|) & (|marking(Client_Sending_17)|=|marking(RequestBuffer_17)|) & (|marking(Client_Sending_25)|=|marking(RequestBuffer_25)|) & (|marking(Client_Sending_29)|=|marking(RequestBuffer_29)|) & (|marking(Client_Sending_2)|=|marking(RequestBuffer_2)|) & (|marking(Client_Sending_12)|=|marking(RequestBuffer_12)|) & (|marking(Client_Sending_38)|=|marking(RequestBuffer_38)|) & (|marking(Client_Sending_48)|=|marking(RequestBuffer_48)|) & (|marking(Client_Sending_42)|=|marking(RequestBuffer_42)|) & (|marking(Client_Sending_7)|=|marking(RequestBuffer_7)|) & (|marking(Client_Sending_32)|=|marking(RequestBuffer_32)|) & (|marking(Client_Sending_35)|=|marking(RequestBuffer_35)|) & (|marking(Client_Sending_49)|=|marking(RequestBuffer_49)|) & (|marking(Client_Sending_44)|=|marking(RequestBuffer_44)|) & (|marking(Client_Sending_30)|=|marking(RequestBuffer_30)|) & (|marking(Client_Sending_39)|=|marking(RequestBuffer_39)|) & (|marking(Client_Sending_26)|=|marking(RequestBuffer_26)|) & (|marking(Client_Sending_33)|=|marking(RequestBuffer_33)|) & (|marking(Client_Sending_10)|=|marking(RequestBuffer_10)|) & (|marking(Client_Sending_14)|=|marking(RequestBuffer_14)|) & (|marking(Client_Sending_41)|=|marking(RequestBuffer_41)|) & (|marking(Client_Sending_3)|=|marking(RequestBuffer_3)|) & (|marking(Client_Sending_18)|=|marking(RequestBuffer_18)|) & (|marking(Client_Sending_21)|=|marking(RequestBuffer_21)|) & (|marking(Client_Sending_45)|=|marking(RequestBuffer_45)|) & (|marking(Client_Sending_20)|=|marking(RequestBuffer_20)|) & (|marking(Client_Sending_43)|=|marking(RequestBuffer_43)|) & (|marking(Client_Sending_16)|=|marking(RequestBuffer_16)|) & (|marking(Client_Sending_15)|=|marking(RequestBuffer_15)|) & (|marking(Client_Sending_37)|=|marking(RequestBuffer_37)|) & (|marking(Client_Sending_28)|=|marking(RequestBuffer_28)|) & (|marking(Client_Sending_6)|=|marking(RequestBuffer_6)|) & (|marking(Client_Sending_27)|=|marking(RequestBuffer_27)|) & (|marking(Client_Sending_47)|=|marking(RequestBuffer_47)|) & (|marking(Client_Sending_9)|=|marking(RequestBuffer_9)|) & (|marking(Client_Sending_46)|=|marking(RequestBuffer_46)|) & (|marking(Client_Sending_13)|=|marking(RequestBuffer_13)|) & (|marking(Client_Sending_11)|=|marking(RequestBuffer_11)|) & (|marking(Client_Sending_8)|=|marking(RequestBuffer_8)|) & (|marking(Client_Sending_19)|=|marking(RequestBuffer_19)|) & (|marking(Client_Sending_34)|=|marking(RequestBuffer_34)|) & (|marking(Client_Sending_24)|=|marking(RequestBuffer_24)|) & (|marking(Client_Sending_31)|=|marking(RequestBuffer_31)|) & (|marking(Client_Sending_1)|=|marking(RequestBuffer_1)|) & (|marking(Client_Sending_36)|=|marking(RequestBuffer_36)|) & (|marking(Client_Sending_4)|=|marking(RequestBuffer_4)|) & (|marking(Client_Sending_5)|=|marking(RequestBuffer_5)|) & (|marking(Client_Sending_40)|=|marking(RequestBuffer_40)|)) & (true & (|marking(RequestBuffer_13)|=|marking(Client_Sending_13)|) & (|marking(RequestBuffer_34)|=|marking(Client_Sending_34)|) & (|marking(RequestBuffer_29)|=|marking(Client_Sending_29)|) & (|marking(RequestBuffer_46)|=|marking(Client_Sending_46)|) & (|marking(RequestBuffer_10)|=|marking(Client_Sending_10)|) & (|marking(RequestBuffer_12)|=|marking(Client_Sending_12)|) & (|marking(RequestBuffer_24)|=|marking(Client_Sending_24)|) & (|marking(RequestBuffer_47)|=|marking(Client_Sending_47)|) & (|marking(RequestBuffer_2)|=|marking(Client_Sending_2)|) & (|marking(RequestBuffer_9)|=|marking(Client_Sending_9)|) & (|marking(RequestBuffer_1)|=|marking(Client_Sending_1)|) & (|marking(RequestBuffer_43)|=|marking(Client_Sending_43)|) & (|marking(RequestBuffer_8)|=|marking(Client_Sending_8)|) & (|marking(RequestBuffer_49)|=|marking(Client_Sending_49)|) & (|marking(RequestBuffer_19)|=|marking(Client_Sending_19)|) & (|marking(RequestBuffer_11)|=|marking(Client_Sending_11)|) & (|marking(RequestBuffer_21)|=|marking(Client_Sending_21)|) & (|marking(RequestBuffer_25)|=|marking(Client_Sending_25)|) & (|marking(RequestBuffer_3)|=|marking(Client_Sending_3)|) & (|marking(RequestBuffer_15)|=|marking(Client_Sending_15)|) & (|marking(RequestBuffer_16)|=|marking(Client_Sending_16)|) & (|marking(RequestBuffer_7)|=|marking(Client_Sending_7)|) & (|marking(RequestBuffer_30)|=|marking(Client_Sending_30)|) & (|marking(RequestBuffer_17)|=|marking(Client_Sending_17)|) & (|marking(RequestBuffer_14)|=|marking(Client_Sending_14)|) & (|marking(RequestBuffer_32)|=|marking(Client_Sending_32)|) & (|marking(RequestBuffer_22)|=|marking(Client_Sending_22)|) & (|marking(RequestBuffer_41)|=|marking(Client_Sending_41)|) & (|marking(RequestBuffer_6)|=|marking(Client_Sending_6)|) & (|marking(RequestBuffer_27)|=|marking(Client_Sending_27)|) & (|marking(RequestBuffer_31)|=|marking(Client_Sending_31)|) & (|marking(RequestBuffer_44)|=|marking(Client_Sending_44)|) & (|marking(RequestBuffer_28)|=|marking(Client_Sending_28)|) & (|marking(RequestBuffer_5)|=|marking(Client_Sending_5)|) & (|marking(RequestBuffer_48)|=|marking(Client_Sending_48)|) & (|marking(RequestBuffer_26)|=|marking(Client_Sending_26)|) & (|marking(RequestBuffer_37)|=|marking(Client_Sending_37)|) & (|marking(RequestBuffer_4)|=|marking(Client_Sending_4)|) & (|marking(RequestBuffer_39)|=|marking(Client_Sending_39)|) & (|marking(RequestBuffer_18)|=|marking(Client_Sending_18)|) & (|marking(RequestBuffer_33)|=|marking(Client_Sending_33)|) & (|marking(RequestBuffer_38)|=|marking(Client_Sending_38)|) & (|marking(RequestBuffer_20)|=|marking(Client_Sending_20)|) & (|marking(RequestBuffer_40)|=|marking(Client_Sending_40)|) & (|marking(RequestBuffer_42)|=|marking(Client_Sending_42)|) & (|marking(RequestBuffer_36)|=|marking(Client_Sending_36)|) & (|marking(RequestBuffer_35)|=|marking(Client_Sending_35)|) & (|marking(RequestBuffer_23)|=|marking(Client_Sending_23)|) & (|marking(RequestBuffer_45)|=|marking(Client_Sending_45)|)))
ctl p_1852_placecomparison_full_or: E F ((true & (|marking(Client_Sending_22)|=|marking(RequestBuffer_22)|) & (|marking(Client_Sending_23)|=|marking(RequestBuffer_23)|) & (|marking(Client_Sending_17)|=|marking(RequestBuffer_17)|) & (|marking(Client_Sending_25)|=|marking(RequestBuffer_25)|) & (|marking(Client_Sending_29)|=|marking(RequestBuffer_29)|) & (|marking(Client_Sending_2)|=|marking(RequestBuffer_2)|) & (|marking(Client_Sending_12)|=|marking(RequestBuffer_12)|) & (|marking(Client_Sending_38)|=|marking(RequestBuffer_38)|) & (|marking(Client_Sending_48)|=|marking(RequestBuffer_48)|) & (|marking(Client_Sending_42)|=|marking(RequestBuffer_42)|) & (|marking(Client_Sending_7)|=|marking(RequestBuffer_7)|) & (|marking(Client_Sending_32)|=|marking(RequestBuffer_32)|) & (|marking(Client_Sending_35)|=|marking(RequestBuffer_35)|) & (|marking(Client_Sending_49)|=|marking(RequestBuffer_49)|) & (|marking(Client_Sending_44)|=|marking(RequestBuffer_44)|) & (|marking(Client_Sending_30)|=|marking(RequestBuffer_30)|) & (|marking(Client_Sending_39)|=|marking(RequestBuffer_39)|) & (|marking(Client_Sending_26)|=|marking(RequestBuffer_26)|) & (|marking(Client_Sending_33)|=|marking(RequestBuffer_33)|) & (|marking(Client_Sending_10)|=|marking(RequestBuffer_10)|) & (|marking(Client_Sending_14)|=|marking(RequestBuffer_14)|) & (|marking(Client_Sending_41)|=|marking(RequestBuffer_41)|) & (|marking(Client_Sending_3)|=|marking(RequestBuffer_3)|) & (|marking(Client_Sending_18)|=|marking(RequestBuffer_18)|) & (|marking(Client_Sending_21)|=|marking(RequestBuffer_21)|) & (|marking(Client_Sending_45)|=|marking(RequestBuffer_45)|) & (|marking(Client_Sending_20)|=|marking(RequestBuffer_20)|) & (|marking(Client_Sending_43)|=|marking(RequestBuffer_43)|) & (|marking(Client_Sending_16)|=|marking(RequestBuffer_16)|) & (|marking(Client_Sending_15)|=|marking(RequestBuffer_15)|) & (|marking(Client_Sending_37)|=|marking(RequestBuffer_37)|) & (|marking(Client_Sending_28)|=|marking(RequestBuffer_28)|) & (|marking(Client_Sending_6)|=|marking(RequestBuffer_6)|) & (|marking(Client_Sending_27)|=|marking(RequestBuffer_27)|) & (|marking(Client_Sending_47)|=|marking(RequestBuffer_47)|) & (|marking(Client_Sending_9)|=|marking(RequestBuffer_9)|) & (|marking(Client_Sending_46)|=|marking(RequestBuffer_46)|) & (|marking(Client_Sending_13)|=|marking(RequestBuffer_13)|) & (|marking(Client_Sending_11)|=|marking(RequestBuffer_11)|) & (|marking(Client_Sending_8)|=|marking(RequestBuffer_8)|) & (|marking(Client_Sending_19)|=|marking(RequestBuffer_19)|) & (|marking(Client_Sending_34)|=|marking(RequestBuffer_34)|) & (|marking(Client_Sending_24)|=|marking(RequestBuffer_24)|) & (|marking(Client_Sending_31)|=|marking(RequestBuffer_31)|) & (|marking(Client_Sending_1)|=|marking(RequestBuffer_1)|) & (|marking(Client_Sending_36)|=|marking(RequestBuffer_36)|) & (|marking(Client_Sending_4)|=|marking(RequestBuffer_4)|) & (|marking(Client_Sending_5)|=|marking(RequestBuffer_5)|) & (|marking(Client_Sending_40)|=|marking(RequestBuffer_40)|)) | (true & (|marking(RequestBuffer_13)|=|marking(Client_Sending_13)|) & (|marking(RequestBuffer_34)|=|marking(Client_Sending_34)|) & (|marking(RequestBuffer_29)|=|marking(Client_Sending_29)|) & (|marking(RequestBuffer_46)|=|marking(Client_Sending_46)|) & (|marking(RequestBuffer_10)|=|marking(Client_Sending_10)|) & (|marking(RequestBuffer_12)|=|marking(Client_Sending_12)|) & (|marking(RequestBuffer_24)|=|marking(Client_Sending_24)|) & (|marking(RequestBuffer_47)|=|marking(Client_Sending_47)|) & (|marking(RequestBuffer_2)|=|marking(Client_Sending_2)|) & (|marking(RequestBuffer_9)|=|marking(Client_Sending_9)|) & (|marking(RequestBuffer_1)|=|marking(Client_Sending_1)|) & (|marking(RequestBuffer_43)|=|marking(Client_Sending_43)|) & (|marking(RequestBuffer_8)|=|marking(Client_Sending_8)|) & (|marking(RequestBuffer_49)|=|marking(Client_Sending_49)|) & (|marking(RequestBuffer_19)|=|marking(Client_Sending_19)|) & (|marking(RequestBuffer_11)|=|marking(Client_Sending_11)|) & (|marking(RequestBuffer_21)|=|marking(Client_Sending_21)|) & (|marking(RequestBuffer_25)|=|marking(Client_Sending_25)|) & (|marking(RequestBuffer_3)|=|marking(Client_Sending_3)|) & (|marking(RequestBuffer_15)|=|marking(Client_Sending_15)|) & (|marking(RequestBuffer_16)|=|marking(Client_Sending_16)|) & (|marking(RequestBuffer_7)|=|marking(Client_Sending_7)|) & (|marking(RequestBuffer_30)|=|marking(Client_Sending_30)|) & (|marking(RequestBuffer_17)|=|marking(Client_Sending_17)|) & (|marking(RequestBuffer_14)|=|marking(Client_Sending_14)|) & (|marking(RequestBuffer_32)|=|marking(Client_Sending_32)|) & (|marking(RequestBuffer_22)|=|marking(Client_Sending_22)|) & (|marking(RequestBuffer_41)|=|marking(Client_Sending_41)|) & (|marking(RequestBuffer_6)|=|marking(Client_Sending_6)|) & (|marking(RequestBuffer_27)|=|marking(Client_Sending_27)|) & (|marking(RequestBuffer_31)|=|marking(Client_Sending_31)|) & (|marking(RequestBuffer_44)|=|marking(Client_Sending_44)|) & (|marking(RequestBuffer_28)|=|marking(Client_Sending_28)|) & (|marking(RequestBuffer_5)|=|marking(Client_Sending_5)|) & (|marking(RequestBuffer_48)|=|marking(Client_Sending_48)|) & (|marking(RequestBuffer_26)|=|marking(Client_Sending_26)|) & (|marking(RequestBuffer_37)|=|marking(Client_Sending_37)|) & (|marking(RequestBuffer_4)|=|marking(Client_Sending_4)|) & (|marking(RequestBuffer_39)|=|marking(Client_Sending_39)|) & (|marking(RequestBuffer_18)|=|marking(Client_Sending_18)|) & (|marking(RequestBuffer_33)|=|marking(Client_Sending_33)|) & (|marking(RequestBuffer_38)|=|marking(Client_Sending_38)|) & (|marking(RequestBuffer_20)|=|marking(Client_Sending_20)|) & (|marking(RequestBuffer_40)|=|marking(Client_Sending_40)|) & (|marking(RequestBuffer_42)|=|marking(Client_Sending_42)|) & (|marking(RequestBuffer_36)|=|marking(Client_Sending_36)|) & (|marking(RequestBuffer_35)|=|marking(Client_Sending_35)|) & (|marking(RequestBuffer_23)|=|marking(Client_Sending_23)|) & (|marking(RequestBuffer_45)|=|marking(Client_Sending_45)|)))
ctl p_1853_placecomparison_full_and_notx: A F ((true & (|marking(Client_Sending_22)|=|marking(RequestBuffer_22)|) & (|marking(Client_Sending_23)|=|marking(RequestBuffer_23)|) & (|marking(Client_Sending_17)|=|marking(RequestBuffer_17)|) & (|marking(Client_Sending_25)|=|marking(RequestBuffer_25)|) & (|marking(Client_Sending_29)|=|marking(RequestBuffer_29)|) & (|marking(Client_Sending_2)|=|marking(RequestBuffer_2)|) & (|marking(Client_Sending_12)|=|marking(RequestBuffer_12)|) & (|marking(Client_Sending_38)|=|marking(RequestBuffer_38)|) & (|marking(Client_Sending_48)|=|marking(RequestBuffer_48)|) & (|marking(Client_Sending_42)|=|marking(RequestBuffer_42)|) & (|marking(Client_Sending_7)|=|marking(RequestBuffer_7)|) & (|marking(Client_Sending_32)|=|marking(RequestBuffer_32)|) & (|marking(Client_Sending_35)|=|marking(RequestBuffer_35)|) & (|marking(Client_Sending_49)|=|marking(RequestBuffer_49)|) & (|marking(Client_Sending_44)|=|marking(RequestBuffer_44)|) & (|marking(Client_Sending_30)|=|marking(RequestBuffer_30)|) & (|marking(Client_Sending_39)|=|marking(RequestBuffer_39)|) & (|marking(Client_Sending_26)|=|marking(RequestBuffer_26)|) & (|marking(Client_Sending_33)|=|marking(RequestBuffer_33)|) & (|marking(Client_Sending_10)|=|marking(RequestBuffer_10)|) & (|marking(Client_Sending_14)|=|marking(RequestBuffer_14)|) & (|marking(Client_Sending_41)|=|marking(RequestBuffer_41)|) & (|marking(Client_Sending_3)|=|marking(RequestBuffer_3)|) & (|marking(Client_Sending_18)|=|marking(RequestBuffer_18)|) & (|marking(Client_Sending_21)|=|marking(RequestBuffer_21)|) & (|marking(Client_Sending_45)|=|marking(RequestBuffer_45)|) & (|marking(Client_Sending_20)|=|marking(RequestBuffer_20)|) & (|marking(Client_Sending_43)|=|marking(RequestBuffer_43)|) & (|marking(Client_Sending_16)|=|marking(RequestBuffer_16)|) & (|marking(Client_Sending_15)|=|marking(RequestBuffer_15)|) & (|marking(Client_Sending_37)|=|marking(RequestBuffer_37)|) & (|marking(Client_Sending_28)|=|marking(RequestBuffer_28)|) & (|marking(Client_Sending_6)|=|marking(RequestBuffer_6)|) & (|marking(Client_Sending_27)|=|marking(RequestBuffer_27)|) & (|marking(Client_Sending_47)|=|marking(RequestBuffer_47)|) & (|marking(Client_Sending_9)|=|marking(RequestBuffer_9)|) & (|marking(Client_Sending_46)|=|marking(RequestBuffer_46)|) & (|marking(Client_Sending_13)|=|marking(RequestBuffer_13)|) & (|marking(Client_Sending_11)|=|marking(RequestBuffer_11)|) & (|marking(Client_Sending_8)|=|marking(RequestBuffer_8)|) & (|marking(Client_Sending_19)|=|marking(RequestBuffer_19)|) & (|marking(Client_Sending_34)|=|marking(RequestBuffer_34)|) & (|marking(Client_Sending_24)|=|marking(RequestBuffer_24)|) & (|marking(Client_Sending_31)|=|marking(RequestBuffer_31)|) & (|marking(Client_Sending_1)|=|marking(RequestBuffer_1)|) & (|marking(Client_Sending_36)|=|marking(RequestBuffer_36)|) & (|marking(Client_Sending_4)|=|marking(RequestBuffer_4)|) & (|marking(Client_Sending_5)|=|marking(RequestBuffer_5)|) & (|marking(Client_Sending_40)|=|marking(RequestBuffer_40)|)) & (true & (|marking(RequestBuffer_13)|=|marking(Client_Sending_13)|) & (|marking(RequestBuffer_34)|=|marking(Client_Sending_34)|) & (|marking(RequestBuffer_29)|=|marking(Client_Sending_29)|) & (|marking(RequestBuffer_46)|=|marking(Client_Sending_46)|) & (|marking(RequestBuffer_10)|=|marking(Client_Sending_10)|) & (|marking(RequestBuffer_12)|=|marking(Client_Sending_12)|) & (|marking(RequestBuffer_24)|=|marking(Client_Sending_24)|) & (|marking(RequestBuffer_47)|=|marking(Client_Sending_47)|) & (|marking(RequestBuffer_2)|=|marking(Client_Sending_2)|) & (|marking(RequestBuffer_9)|=|marking(Client_Sending_9)|) & (|marking(RequestBuffer_1)|=|marking(Client_Sending_1)|) & (|marking(RequestBuffer_43)|=|marking(Client_Sending_43)|) & (|marking(RequestBuffer_8)|=|marking(Client_Sending_8)|) & (|marking(RequestBuffer_49)|=|marking(Client_Sending_49)|) & (|marking(RequestBuffer_19)|=|marking(Client_Sending_19)|) & (|marking(RequestBuffer_11)|=|marking(Client_Sending_11)|) & (|marking(RequestBuffer_21)|=|marking(Client_Sending_21)|) & (|marking(RequestBuffer_25)|=|marking(Client_Sending_25)|) & (|marking(RequestBuffer_3)|=|marking(Client_Sending_3)|) & (|marking(RequestBuffer_15)|=|marking(Client_Sending_15)|) & (|marking(RequestBuffer_16)|=|marking(Client_Sending_16)|) & (|marking(RequestBuffer_7)|=|marking(Client_Sending_7)|) & (|marking(RequestBuffer_30)|=|marking(Client_Sending_30)|) & (|marking(RequestBuffer_17)|=|marking(Client_Sending_17)|) & (|marking(RequestBuffer_14)|=|marking(Client_Sending_14)|) & (|marking(RequestBuffer_32)|=|marking(Client_Sending_32)|) & (|marking(RequestBuffer_22)|=|marking(Client_Sending_22)|) & (|marking(RequestBuffer_41)|=|marking(Client_Sending_41)|) & (|marking(RequestBuffer_6)|=|marking(Client_Sending_6)|) & (|marking(RequestBuffer_27)|=|marking(Client_Sending_27)|) & (|marking(RequestBuffer_31)|=|marking(Client_Sending_31)|) & (|marking(RequestBuffer_44)|=|marking(Client_Sending_44)|) & (|marking(RequestBuffer_28)|=|marking(Client_Sending_28)|) & (|marking(RequestBuffer_5)|=|marking(Client_Sending_5)|) & (|marking(RequestBuffer_48)|=|marking(Client_Sending_48)|) & (|marking(RequestBuffer_26)|=|marking(Client_Sending_26)|) & (|marking(RequestBuffer_37)|=|marking(Client_Sending_37)|) & (|marking(RequestBuffer_4)|=|marking(Client_Sending_4)|) & (|marking(RequestBuffer_39)|=|marking(Client_Sending_39)|) & (|marking(RequestBuffer_18)|=|marking(Client_Sending_18)|) & (|marking(RequestBuffer_33)|=|marking(Client_Sending_33)|) & (|marking(RequestBuffer_38)|=|marking(Client_Sending_38)|) & (|marking(RequestBuffer_20)|=|marking(Client_Sending_20)|) & (|marking(RequestBuffer_40)|=|marking(Client_Sending_40)|) & (|marking(RequestBuffer_42)|=|marking(Client_Sending_42)|) & (|marking(RequestBuffer_36)|=|marking(Client_Sending_36)|) & (|marking(RequestBuffer_35)|=|marking(Client_Sending_35)|) & (|marking(RequestBuffer_23)|=|marking(Client_Sending_23)|) & (|marking(RequestBuffer_45)|=|marking(Client_Sending_45)|)))


--------------------
content from /tmp/BenchKit_head_log_file.1659: