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=Peterson-PT-4
export BK_EXAMINATION=CTLPlaceComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1658
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/Peterson-PT-4
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is Peterson-PT-4, examination is CTLPlaceComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for Peterson/4 (P/T)

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

execution on node 38: cluster1u40.lip6.fr (runId=136966892601329_n_38)
=====================================================================
runnning marcie on Peterson-PT-4 (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 Peterson-PT-4, examination is CTLPlaceComparison
=====================================================================

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

START 1369698478

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: 480 NrTr: 690)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369698478

--------------------
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: A F (X (true & (|marking(TestAlone_0_1_2)|!=|marking(TestIdentity_0_1_2)|) & (|marking(TestAlone_0_2_2)|!=|marking(TestIdentity_0_2_2)|) & (|marking(TestAlone_0_3_1)|!=|marking(TestIdentity_0_3_1)|) & (|marking(TestAlone_4_0_2)|!=|marking(TestIdentity_4_0_2)|) & (|marking(TestAlone_3_1_1)|!=|marking(TestIdentity_3_1_1)|) & (|marking(TestAlone_1_3_4)|!=|marking(TestIdentity_1_3_4)|) & (|marking(TestAlone_4_2_3)|!=|marking(TestIdentity_4_2_3)|) & (|marking(TestAlone_3_0_2)|!=|marking(TestIdentity_3_0_2)|) & (|marking(TestAlone_0_0_4)|!=|marking(TestIdentity_0_0_4)|) & (|marking(TestAlone_4_3_2)|!=|marking(TestIdentity_4_3_2)|) & (|marking(TestAlone_1_2_0)|!=|marking(TestIdentity_1_2_0)|) & (|marking(TestAlone_3_1_4)|!=|marking(TestIdentity_3_1_4)|) & (|marking(TestAlone_1_3_2)|!=|marking(TestIdentity_1_3_2)|) & (|marking(TestAlone_3_0_1)|!=|marking(TestIdentity_3_0_1)|) & (|marking(TestAlone_2_3_3)|!=|marking(TestIdentity_2_3_3)|) & (|marking(TestAlone_2_0_3)|!=|marking(TestIdentity_2_0_3)|) & (|marking(TestAlone_2_1_0)|!=|marking(TestIdentity_2_1_0)|) & (|marking(TestAlone_0_1_3)|!=|marking(TestIdentity_0_1_3)|) & (|marking(TestAlone_0_3_3)|!=|marking(TestIdentity_0_3_3)|) & (|marking(TestAlone_2_0_1)|!=|marking(TestIdentity_2_0_1)|) & (|marking(TestAlone_1_0_3)|!=|marking(TestIdentity_1_0_3)|) & (|marking(TestAlone_1_1_3)|!=|marking(TestIdentity_1_1_3)|) & (|marking(TestAlone_0_2_1)|!=|marking(TestIdentity_0_2_1)|) & (|marking(TestAlone_0_2_4)|!=|marking(TestIdentity_0_2_4)|) & (|marking(TestAlone_4_1_3)|!=|marking(TestIdentity_4_1_3)|) & (|marking(TestAlone_3_3_4)|!=|marking(TestIdentity_3_3_4)|) & (|marking(TestAlone_4_1_0)|!=|marking(TestIdentity_4_1_0)|) & (|marking(TestAlone_1_2_4)|!=|marking(TestIdentity_1_2_4)|) & (|marking(TestAlone_0_0_2)|!=|marking(TestIdentity_0_0_2)|) & (|marking(TestAlone_2_0_4)|!=|marking(TestIdentity_2_0_4)|) & (|marking(TestAlone_1_1_2)|!=|marking(TestIdentity_1_1_2)|) & (|marking(TestAlone_2_2_1)|!=|marking(TestIdentity_2_2_1)|) & (|marking(TestAlone_3_3_1)|!=|marking(TestIdentity_3_3_1)|) & (|marking(TestAlone_0_0_3)|!=|marking(TestIdentity_0_0_3)|) & (|marking(TestAlone_1_0_0)|!=|marking(TestIdentity_1_0_0)|) & (|marking(TestAlone_4_3_3)|!=|marking(TestIdentity_4_3_3)|) & (|marking(TestAlone_4_2_1)|!=|marking(TestIdentity_4_2_1)|) & (|marking(TestAlone_2_2_0)|!=|marking(TestIdentity_2_2_0)|) & (|marking(TestAlone_2_1_4)|!=|marking(TestIdentity_2_1_4)|) & (|marking(TestAlone_1_3_3)|!=|marking(TestIdentity_1_3_3)|) & (|marking(TestAlone_2_3_4)|!=|marking(TestIdentity_2_3_4)|) & (|marking(TestAlone_4_3_0)|!=|marking(TestIdentity_4_3_0)|) & (|marking(TestAlone_3_3_0)|!=|marking(TestIdentity_3_3_0)|) & (|marking(TestAlone_4_0_0)|!=|marking(TestIdentity_4_0_0)|) & (|marking(TestAlone_0_3_2)|!=|marking(TestIdentity_0_3_2)|) & (|marking(TestAlone_4_1_2)|!=|marking(TestIdentity_4_1_2)|) & (|marking(TestAlone_3_1_0)|!=|marking(TestIdentity_3_1_0)|) & (|marking(TestAlone_3_0_0)|!=|marking(TestIdentity_3_0_0)|) & (|marking(TestAlone_3_2_0)|!=|marking(TestIdentity_3_2_0)|) & (|marking(TestAlone_1_2_3)|!=|marking(TestIdentity_1_2_3)|) & (|marking(TestAlone_3_1_2)|!=|marking(TestIdentity_3_1_2)|) & (|marking(TestAlone_3_2_4)|!=|marking(TestIdentity_3_2_4)|) & (|marking(TestAlone_1_0_4)|!=|marking(TestIdentity_1_0_4)|) & (|marking(TestAlone_2_3_1)|!=|marking(TestIdentity_2_3_1)|) & (|marking(TestAlone_0_0_1)|!=|marking(TestIdentity_0_0_1)|) & (|marking(TestAlone_0_3_4)|!=|marking(TestIdentity_0_3_4)|) & (|marking(TestAlone_0_1_4)|!=|marking(TestIdentity_0_1_4)|) & (|marking(TestAlone_1_0_2)|!=|marking(TestIdentity_1_0_2)|) & (|marking(TestAlone_2_2_4)|!=|marking(TestIdentity_2_2_4)|) & (|marking(TestAlone_0_1_1)|!=|marking(TestIdentity_0_1_1)|) & (|marking(TestAlone_1_3_0)|!=|marking(TestIdentity_1_3_0)|) & (|marking(TestAlone_2_3_0)|!=|marking(TestIdentity_2_3_0)|) & (|marking(TestAlone_4_2_2)|!=|marking(TestIdentity_4_2_2)|) & (|marking(TestAlone_3_0_4)|!=|marking(TestIdentity_3_0_4)|) & (|marking(TestAlone_0_2_3)|!=|marking(TestIdentity_0_2_3)|) & (|marking(TestAlone_1_1_4)|!=|marking(TestIdentity_1_1_4)|) & (|marking(TestAlone_2_2_3)|!=|marking(TestIdentity_2_2_3)|) & (|marking(TestAlone_3_2_1)|!=|marking(TestIdentity_3_2_1)|) & (|marking(TestAlone_1_1_0)|!=|marking(TestIdentity_1_1_0)|) & (|marking(TestAlone_4_2_0)|!=|marking(TestIdentity_4_2_0)|) & (|marking(TestAlone_3_2_2)|!=|marking(TestIdentity_3_2_2)|) & (|marking(TestAlone_3_3_2)|!=|marking(TestIdentity_3_3_2)|) & (|marking(TestAlone_2_1_3)|!=|marking(TestIdentity_2_1_3)|) & (|marking(TestAlone_4_0_1)|!=|marking(TestIdentity_4_0_1)|) & (|marking(TestAlone_2_1_1)|!=|marking(TestIdentity_2_1_1)|) & (|marking(TestAlone_2_0_0)|!=|marking(TestIdentity_2_0_0)|) & (|marking(TestAlone_4_1_1)|!=|marking(TestIdentity_4_1_1)|) & (|marking(TestAlone_4_3_1)|!=|marking(TestIdentity_4_3_1)|) & (|marking(TestAlone_1_2_2)|!=|marking(TestIdentity_1_2_2)|) & (|marking(TestAlone_4_0_3)|!=|marking(TestIdentity_4_0_3)|) & (|marking(TestIdentity_3_2_3)|!=0) & (|marking(TestIdentity_0_0_0)|!=0) & (|marking(TestIdentity_0_2_0)|!=0) & (|marking(TestIdentity_0_3_0)|!=0) & (|marking(TestIdentity_4_0_4)|!=0) & (|marking(TestIdentity_4_1_4)|!=0) & (|marking(TestIdentity_3_3_3)|!=0) & (|marking(TestIdentity_4_3_4)|!=0) & (|marking(TestIdentity_3_1_3)|!=0) & (|marking(TestIdentity_4_2_4)|!=0) & (|marking(TestIdentity_1_3_1)|!=0) & (|marking(TestIdentity_3_0_3)|!=0) & (|marking(TestIdentity_2_2_2)|!=0) & (|marking(TestIdentity_2_3_2)|!=0) & (|marking(TestIdentity_0_1_0)|!=0) & (|marking(TestIdentity_1_2_1)|!=0) & (|marking(TestIdentity_2_1_2)|!=0) & (|marking(TestIdentity_1_1_1)|!=0) & (|marking(TestIdentity_1_0_1)|!=0) & (|marking(TestIdentity_2_0_2)|!=0)) | X (true & (|marking(AskForSection_4_3)|!=|marking(EndTurn_4_3)|) & (|marking(AskForSection_0_1)|!=|marking(EndTurn_0_1)|) & (|marking(AskForSection_0_3)|!=|marking(EndTurn_0_3)|) & (|marking(AskForSection_1_1)|!=|marking(EndTurn_1_1)|) & (|marking(AskForSection_2_1)|!=|marking(EndTurn_2_1)|) & (|marking(AskForSection_3_2)|!=|marking(EndTurn_3_2)|) & (|marking(AskForSection_1_3)|!=|marking(EndTurn_1_3)|) & (|marking(AskForSection_0_0)|!=|marking(EndTurn_0_0)|) & (|marking(AskForSection_2_0)|!=|marking(EndTurn_2_0)|) & (|marking(AskForSection_4_1)|!=|marking(EndTurn_4_1)|) & (|marking(AskForSection_3_3)|!=|marking(EndTurn_3_3)|) & (|marking(AskForSection_1_2)|!=|marking(EndTurn_1_2)|) & (|marking(AskForSection_0_2)|!=|marking(EndTurn_0_2)|) & (|marking(AskForSection_4_2)|!=|marking(EndTurn_4_2)|) & (|marking(AskForSection_4_0)|!=|marking(EndTurn_4_0)|) & (|marking(AskForSection_3_1)|!=|marking(EndTurn_3_1)|) & (|marking(AskForSection_2_3)|!=|marking(EndTurn_2_3)|) & (|marking(AskForSection_3_0)|!=|marking(EndTurn_3_0)|) & (|marking(AskForSection_2_2)|!=|marking(EndTurn_2_2)|) & (|marking(AskForSection_1_0)|!=|marking(EndTurn_1_0)|)))
ctl p_1851_placecomparison_full_and: A G ((true & (|marking(TestIdentity_3_2_4)|!=|marking(TestAlone_3_2_4)|) & (|marking(TestIdentity_3_3_0)|!=|marking(TestAlone_3_3_0)|) & (|marking(TestIdentity_1_2_3)|!=|marking(TestAlone_1_2_3)|) & (|marking(TestIdentity_1_1_4)|!=|marking(TestAlone_1_1_4)|) & (|marking(TestIdentity_4_3_0)|!=|marking(TestAlone_4_3_0)|) & (|marking(TestIdentity_1_2_2)|!=|marking(TestAlone_1_2_2)|) & (|marking(TestIdentity_3_3_2)|!=|marking(TestAlone_3_3_2)|) & (|marking(TestIdentity_0_0_3)|!=|marking(TestAlone_0_0_3)|) & (|marking(TestIdentity_4_0_0)|!=|marking(TestAlone_4_0_0)|) & (|marking(TestIdentity_3_2_0)|!=|marking(TestAlone_3_2_0)|) & (|marking(TestIdentity_3_1_2)|!=|marking(TestAlone_3_1_2)|) & (|marking(TestIdentity_4_3_3)|!=|marking(TestAlone_4_3_3)|) & (|marking(TestIdentity_3_0_2)|!=|marking(TestAlone_3_0_2)|) & (|marking(TestIdentity_4_1_1)|!=|marking(TestAlone_4_1_1)|) & (|marking(TestIdentity_0_1_2)|!=|marking(TestAlone_0_1_2)|) & (|marking(TestIdentity_2_2_1)|!=|marking(TestAlone_2_2_1)|) & (|marking(TestIdentity_0_3_2)|!=|marking(TestAlone_0_3_2)|) & (|marking(TestIdentity_2_1_3)|!=|marking(TestAlone_2_1_3)|) & (|marking(TestIdentity_0_2_1)|!=|marking(TestAlone_0_2_1)|) & (|marking(TestIdentity_4_3_1)|!=|marking(TestAlone_4_3_1)|) & (|marking(TestIdentity_4_2_1)|!=|marking(TestAlone_4_2_1)|) & (|marking(TestIdentity_0_1_4)|!=|marking(TestAlone_0_1_4)|) & (|marking(TestIdentity_2_2_4)|!=|marking(TestAlone_2_2_4)|) & (|marking(TestIdentity_2_0_3)|!=|marking(TestAlone_2_0_3)|) & (|marking(TestIdentity_4_0_3)|!=|marking(TestAlone_4_0_3)|) & (|marking(TestIdentity_4_0_2)|!=|marking(TestAlone_4_0_2)|) & (|marking(TestIdentity_0_1_3)|!=|marking(TestAlone_0_1_3)|) & (|marking(TestIdentity_3_1_0)|!=|marking(TestAlone_3_1_0)|) & (|marking(TestIdentity_3_3_4)|!=|marking(TestAlone_3_3_4)|) & (|marking(TestIdentity_1_0_4)|!=|marking(TestAlone_1_0_4)|) & (|marking(TestIdentity_2_0_0)|!=|marking(TestAlone_2_0_0)|) & (|marking(TestIdentity_3_3_1)|!=|marking(TestAlone_3_3_1)|) & (|marking(TestIdentity_0_3_1)|!=|marking(TestAlone_0_3_1)|) & (|marking(TestIdentity_2_3_4)|!=|marking(TestAlone_2_3_4)|) & (|marking(TestIdentity_4_1_2)|!=|marking(TestAlone_4_1_2)|) & (|marking(TestIdentity_3_1_4)|!=|marking(TestAlone_3_1_4)|) & (|marking(TestIdentity_1_0_2)|!=|marking(TestAlone_1_0_2)|) & (|marking(TestIdentity_0_3_3)|!=|marking(TestAlone_0_3_3)|) & (|marking(TestIdentity_0_3_4)|!=|marking(TestAlone_0_3_4)|) & (|marking(TestIdentity_3_2_2)|!=|marking(TestAlone_3_2_2)|) & (|marking(TestIdentity_0_2_3)|!=|marking(TestAlone_0_2_3)|) & (|marking(TestIdentity_4_2_3)|!=|marking(TestAlone_4_2_3)|) & (|marking(TestIdentity_1_1_3)|!=|marking(TestAlone_1_1_3)|) & (|marking(TestIdentity_2_0_1)|!=|marking(TestAlone_2_0_1)|) & (|marking(TestIdentity_1_2_4)|!=|marking(TestAlone_1_2_4)|) & (|marking(TestIdentity_4_1_0)|!=|marking(TestAlone_4_1_0)|) & (|marking(TestIdentity_1_0_3)|!=|marking(TestAlone_1_0_3)|) & (|marking(TestIdentity_2_2_0)|!=|marking(TestAlone_2_2_0)|) & (|marking(TestIdentity_4_2_2)|!=|marking(TestAlone_4_2_2)|) & (|marking(TestIdentity_0_1_1)|!=|marking(TestAlone_0_1_1)|) & (|marking(TestIdentity_2_0_4)|!=|marking(TestAlone_2_0_4)|) & (|marking(TestIdentity_1_1_0)|!=|marking(TestAlone_1_1_0)|) & (|marking(TestIdentity_2_1_0)|!=|marking(TestAlone_2_1_0)|) & (|marking(TestIdentity_3_0_4)|!=|marking(TestAlone_3_0_4)|) & (|marking(TestIdentity_0_0_2)|!=|marking(TestAlone_0_0_2)|) & (|marking(TestIdentity_1_3_3)|!=|marking(TestAlone_1_3_3)|) & (|marking(TestIdentity_2_1_4)|!=|marking(TestAlone_2_1_4)|) & (|marking(TestIdentity_0_2_2)|!=|marking(TestAlone_0_2_2)|) & (|marking(TestIdentity_2_3_3)|!=|marking(TestAlone_2_3_3)|) & (|marking(TestIdentity_3_1_1)|!=|marking(TestAlone_3_1_1)|) & (|marking(TestIdentity_2_3_0)|!=|marking(TestAlone_2_3_0)|) & (|marking(TestIdentity_1_3_0)|!=|marking(TestAlone_1_3_0)|) & (|marking(TestIdentity_0_2_4)|!=|marking(TestAlone_0_2_4)|) & (|marking(TestIdentity_2_1_1)|!=|marking(TestAlone_2_1_1)|) & (|marking(TestIdentity_3_2_1)|!=|marking(TestAlone_3_2_1)|) & (|marking(TestIdentity_3_0_0)|!=|marking(TestAlone_3_0_0)|) & (|marking(TestIdentity_3_0_1)|!=|marking(TestAlone_3_0_1)|) & (|marking(TestIdentity_4_1_3)|!=|marking(TestAlone_4_1_3)|) & (|marking(TestIdentity_1_0_0)|!=|marking(TestAlone_1_0_0)|) & (|marking(TestIdentity_0_0_1)|!=|marking(TestAlone_0_0_1)|) & (|marking(TestIdentity_4_3_2)|!=|marking(TestAlone_4_3_2)|) & (|marking(TestIdentity_4_0_1)|!=|marking(TestAlone_4_0_1)|) & (|marking(TestIdentity_2_2_3)|!=|marking(TestAlone_2_2_3)|) & (|marking(TestIdentity_1_3_4)|!=|marking(TestAlone_1_3_4)|) & (|marking(TestIdentity_0_0_4)|!=|marking(TestAlone_0_0_4)|) & (|marking(TestIdentity_1_2_0)|!=|marking(TestAlone_1_2_0)|) & (|marking(TestIdentity_1_3_2)|!=|marking(TestAlone_1_3_2)|) & (|marking(TestIdentity_1_1_2)|!=|marking(TestAlone_1_1_2)|) & (|marking(TestIdentity_4_2_0)|!=|marking(TestAlone_4_2_0)|) & (|marking(TestIdentity_2_3_1)|!=|marking(TestAlone_2_3_1)|) & (|marking(TestIdentity_3_2_3)|!=0) & (|marking(TestIdentity_0_0_0)|!=0) & (|marking(TestIdentity_0_2_0)|!=0) & (|marking(TestIdentity_0_3_0)|!=0) & (|marking(TestIdentity_4_0_4)|!=0) & (|marking(TestIdentity_4_1_4)|!=0) & (|marking(TestIdentity_3_3_3)|!=0) & (|marking(TestIdentity_4_3_4)|!=0) & (|marking(TestIdentity_3_1_3)|!=0) & (|marking(TestIdentity_4_2_4)|!=0) & (|marking(TestIdentity_1_3_1)|!=0) & (|marking(TestIdentity_3_0_3)|!=0) & (|marking(TestIdentity_2_2_2)|!=0) & (|marking(TestIdentity_2_3_2)|!=0) & (|marking(TestIdentity_0_1_0)|!=0) & (|marking(TestIdentity_1_2_1)|!=0) & (|marking(TestIdentity_2_1_2)|!=0) & (|marking(TestIdentity_1_1_1)|!=0) & (|marking(TestIdentity_1_0_1)|!=0) & (|marking(TestIdentity_2_0_2)|!=0)) & ((true) & (true & (|marking(BeginLoop_1_3_1)|<=|marking(IsEndLoop_1_3_1)|) & (|marking(BeginLoop_4_1_3)|<=|marking(IsEndLoop_4_1_3)|) & (|marking(BeginLoop_1_0_1)|<=|marking(IsEndLoop_1_0_1)|) & (|marking(BeginLoop_0_2_4)|<=|marking(IsEndLoop_0_2_4)|) & (|marking(BeginLoop_0_0_0)|<=|marking(IsEndLoop_0_0_0)|) & (|marking(BeginLoop_2_1_2)|<=|marking(IsEndLoop_2_1_2)|) & (|marking(BeginLoop_0_1_3)|<=|marking(IsEndLoop_0_1_3)|) & (|marking(BeginLoop_1_2_0)|<=|marking(IsEndLoop_1_2_0)|) & (|marking(BeginLoop_0_3_3)|<=|marking(IsEndLoop_0_3_3)|) & (|marking(BeginLoop_4_0_1)|<=|marking(IsEndLoop_4_0_1)|) & (|marking(BeginLoop_4_1_1)|<=|marking(IsEndLoop_4_1_1)|) & (|marking(BeginLoop_4_1_0)|<=|marking(IsEndLoop_4_1_0)|) & (|marking(BeginLoop_3_1_1)|<=|marking(IsEndLoop_3_1_1)|) & (|marking(BeginLoop_1_1_2)|<=|marking(IsEndLoop_1_1_2)|) & (|marking(BeginLoop_0_1_0)|<=|marking(IsEndLoop_0_1_0)|) & (|marking(BeginLoop_3_1_2)|<=|marking(IsEndLoop_3_1_2)|) & (|marking(BeginLoop_1_2_2)|<=|marking(IsEndLoop_1_2_2)|) & (|marking(BeginLoop_0_3_0)|<=|marking(IsEndLoop_0_3_0)|) & (|marking(BeginLoop_2_2_0)|<=|marking(IsEndLoop_2_2_0)|) & (|marking(BeginLoop_4_0_2)|<=|marking(IsEndLoop_4_0_2)|) & (|marking(BeginLoop_1_2_4)|<=|marking(IsEndLoop_1_2_4)|) & (|marking(BeginLoop_2_1_1)|<=|marking(IsEndLoop_2_1_1)|) & (|marking(BeginLoop_1_3_3)|<=|marking(IsEndLoop_1_3_3)|) & (|marking(BeginLoop_4_3_4)|<=|marking(IsEndLoop_4_3_4)|) & (|marking(BeginLoop_3_3_2)|<=|marking(IsEndLoop_3_3_2)|) & (|marking(BeginLoop_4_1_4)|<=|marking(IsEndLoop_4_1_4)|) & (|marking(BeginLoop_2_0_4)|<=|marking(IsEndLoop_2_0_4)|) & (|marking(BeginLoop_1_3_0)|<=|marking(IsEndLoop_1_3_0)|) & (|marking(BeginLoop_0_1_2)|<=|marking(IsEndLoop_0_1_2)|) & (|marking(BeginLoop_0_1_1)|<=|marking(IsEndLoop_0_1_1)|) & (|marking(BeginLoop_4_2_4)|<=|marking(IsEndLoop_4_2_4)|) & (|marking(BeginLoop_1_0_0)|<=|marking(IsEndLoop_1_0_0)|) & (|marking(BeginLoop_0_2_2)|<=|marking(IsEndLoop_0_2_2)|) & (|marking(BeginLoop_2_2_4)|<=|marking(IsEndLoop_2_2_4)|) & (|marking(BeginLoop_3_3_1)|<=|marking(IsEndLoop_3_3_1)|) & (|marking(BeginLoop_2_3_2)|<=|marking(IsEndLoop_2_3_2)|) & (|marking(BeginLoop_4_2_0)|<=|marking(IsEndLoop_4_2_0)|) & (|marking(BeginLoop_1_3_4)|<=|marking(IsEndLoop_1_3_4)|) & (|marking(BeginLoop_4_2_2)|<=|marking(IsEndLoop_4_2_2)|) & (|marking(BeginLoop_2_0_3)|<=|marking(IsEndLoop_2_0_3)|) & (|marking(BeginLoop_0_2_1)|<=|marking(IsEndLoop_0_2_1)|) & (|marking(BeginLoop_3_1_4)|<=|marking(IsEndLoop_3_1_4)|) & (|marking(BeginLoop_4_1_2)|<=|marking(IsEndLoop_4_1_2)|) & (|marking(BeginLoop_3_2_4)|<=|marking(IsEndLoop_3_2_4)|) & (|marking(BeginLoop_3_2_2)|<=|marking(IsEndLoop_3_2_2)|) & (|marking(BeginLoop_2_0_2)|<=|marking(IsEndLoop_2_0_2)|) & (|marking(BeginLoop_3_3_3)|<=|marking(IsEndLoop_3_3_3)|) & (|marking(BeginLoop_0_3_2)|<=|marking(IsEndLoop_0_3_2)|) & (|marking(BeginLoop_2_2_2)|<=|marking(IsEndLoop_2_2_2)|) & (|marking(BeginLoop_2_3_3)|<=|marking(IsEndLoop_2_3_3)|) & (|marking(BeginLoop_4_3_0)|<=|marking(IsEndLoop_4_3_0)|) & (|marking(BeginLoop_4_2_3)|<=|marking(IsEndLoop_4_2_3)|) & (|marking(BeginLoop_4_0_3)|<=|marking(IsEndLoop_4_0_3)|) & (|marking(BeginLoop_2_1_4)|<=|marking(IsEndLoop_2_1_4)|) & (|marking(BeginLoop_3_2_1)|<=|marking(IsEndLoop_3_2_1)|) & (|marking(BeginLoop_2_0_0)|<=|marking(IsEndLoop_2_0_0)|) & (|marking(BeginLoop_4_0_4)|<=|marking(IsEndLoop_4_0_4)|) & (|marking(BeginLoop_1_1_0)|<=|marking(IsEndLoop_1_1_0)|) & (|marking(BeginLoop_3_3_0)|<=|marking(IsEndLoop_3_3_0)|) & (|marking(BeginLoop_1_1_3)|<=|marking(IsEndLoop_1_1_3)|) & (|marking(BeginLoop_0_0_3)|<=|marking(IsEndLoop_0_0_3)|) & (|marking(BeginLoop_3_0_3)|<=|marking(IsEndLoop_3_0_3)|) & (|marking(BeginLoop_3_2_3)|<=|marking(IsEndLoop_3_2_3)|) & (|marking(BeginLoop_2_3_0)|<=|marking(IsEndLoop_2_3_0)|) & (|marking(BeginLoop_1_1_1)|<=|marking(IsEndLoop_1_1_1)|) & (|marking(BeginLoop_0_0_1)|<=|marking(IsEndLoop_0_0_1)|) & (|marking(BeginLoop_3_0_2)|<=|marking(IsEndLoop_3_0_2)|) & (|marking(BeginLoop_4_3_1)|<=|marking(IsEndLoop_4_3_1)|) & (|marking(BeginLoop_2_1_0)|<=|marking(IsEndLoop_2_1_0)|) & (|marking(BeginLoop_3_1_3)|<=|marking(IsEndLoop_3_1_3)|) & (|marking(BeginLoop_1_0_4)|<=|marking(IsEndLoop_1_0_4)|) & (|marking(BeginLoop_3_0_0)|<=|marking(IsEndLoop_3_0_0)|) & (|marking(BeginLoop_2_2_1)|<=|marking(IsEndLoop_2_2_1)|) & (|marking(BeginLoop_1_2_1)|<=|marking(IsEndLoop_1_2_1)|) & (|marking(BeginLoop_2_3_1)|<=|marking(IsEndLoop_2_3_1)|) & (|marking(BeginLoop_1_1_4)|<=|marking(IsEndLoop_1_1_4)|) & (|marking(BeginLoop_1_0_3)|<=|marking(IsEndLoop_1_0_3)|) & (|marking(BeginLoop_3_0_4)|<=|marking(IsEndLoop_3_0_4)|) & (|marking(BeginLoop_1_0_2)|<=|marking(IsEndLoop_1_0_2)|) & (|marking(BeginLoop_3_1_0)|<=|marking(IsEndLoop_3_1_0)|) & (|marking(BeginLoop_4_3_3)|<=|marking(IsEndLoop_4_3_3)|) & (|marking(BeginLoop_3_3_4)|<=|marking(IsEndLoop_3_3_4)|) & (|marking(BeginLoop_2_1_3)|<=|marking(IsEndLoop_2_1_3)|) & (|marking(BeginLoop_0_3_1)|<=|marking(IsEndLoop_0_3_1)|) & (|marking(BeginLoop_4_2_1)|<=|marking(IsEndLoop_4_2_1)|) & (|marking(BeginLoop_3_2_0)|<=|marking(IsEndLoop_3_2_0)|) & (|marking(BeginLoop_0_0_2)|<=|marking(IsEndLoop_0_0_2)|) & (|marking(BeginLoop_1_3_2)|<=|marking(IsEndLoop_1_3_2)|) & (|marking(BeginLoop_2_3_4)|<=|marking(IsEndLoop_2_3_4)|) & (|marking(BeginLoop_2_2_3)|<=|marking(IsEndLoop_2_2_3)|) & (|marking(BeginLoop_0_0_4)|<=|marking(IsEndLoop_0_0_4)|) & (|marking(BeginLoop_0_3_4)|<=|marking(IsEndLoop_0_3_4)|) & (|marking(BeginLoop_0_2_0)|<=|marking(IsEndLoop_0_2_0)|) & (|marking(BeginLoop_0_1_4)|<=|marking(IsEndLoop_0_1_4)|) & (|marking(BeginLoop_2_0_1)|<=|marking(IsEndLoop_2_0_1)|) & (|marking(BeginLoop_0_2_3)|<=|marking(IsEndLoop_0_2_3)|) & (|marking(BeginLoop_4_3_2)|<=|marking(IsEndLoop_4_3_2)|) & (|marking(BeginLoop_1_2_3)|<=|marking(IsEndLoop_1_2_3)|) & (|marking(BeginLoop_3_0_1)|<=|marking(IsEndLoop_3_0_1)|) & (|marking(BeginLoop_4_0_0)|<=|marking(IsEndLoop_4_0_0)|))))
ctl p_1852_placecomparison_full_or: A F ((true & (|marking(TestIdentity_3_2_4)|!=|marking(TestAlone_3_2_4)|) & (|marking(TestIdentity_3_3_0)|!=|marking(TestAlone_3_3_0)|) & (|marking(TestIdentity_1_2_3)|!=|marking(TestAlone_1_2_3)|) & (|marking(TestIdentity_1_1_4)|!=|marking(TestAlone_1_1_4)|) & (|marking(TestIdentity_4_3_0)|!=|marking(TestAlone_4_3_0)|) & (|marking(TestIdentity_1_2_2)|!=|marking(TestAlone_1_2_2)|) & (|marking(TestIdentity_3_3_2)|!=|marking(TestAlone_3_3_2)|) & (|marking(TestIdentity_0_0_3)|!=|marking(TestAlone_0_0_3)|) & (|marking(TestIdentity_4_0_0)|!=|marking(TestAlone_4_0_0)|) & (|marking(TestIdentity_3_2_0)|!=|marking(TestAlone_3_2_0)|) & (|marking(TestIdentity_3_1_2)|!=|marking(TestAlone_3_1_2)|) & (|marking(TestIdentity_4_3_3)|!=|marking(TestAlone_4_3_3)|) & (|marking(TestIdentity_3_0_2)|!=|marking(TestAlone_3_0_2)|) & (|marking(TestIdentity_4_1_1)|!=|marking(TestAlone_4_1_1)|) & (|marking(TestIdentity_0_1_2)|!=|marking(TestAlone_0_1_2)|) & (|marking(TestIdentity_2_2_1)|!=|marking(TestAlone_2_2_1)|) & (|marking(TestIdentity_0_3_2)|!=|marking(TestAlone_0_3_2)|) & (|marking(TestIdentity_2_1_3)|!=|marking(TestAlone_2_1_3)|) & (|marking(TestIdentity_0_2_1)|!=|marking(TestAlone_0_2_1)|) & (|marking(TestIdentity_4_3_1)|!=|marking(TestAlone_4_3_1)|) & (|marking(TestIdentity_4_2_1)|!=|marking(TestAlone_4_2_1)|) & (|marking(TestIdentity_0_1_4)|!=|marking(TestAlone_0_1_4)|) & (|marking(TestIdentity_2_2_4)|!=|marking(TestAlone_2_2_4)|) & (|marking(TestIdentity_2_0_3)|!=|marking(TestAlone_2_0_3)|) & (|marking(TestIdentity_4_0_3)|!=|marking(TestAlone_4_0_3)|) & (|marking(TestIdentity_4_0_2)|!=|marking(TestAlone_4_0_2)|) & (|marking(TestIdentity_0_1_3)|!=|marking(TestAlone_0_1_3)|) & (|marking(TestIdentity_3_1_0)|!=|marking(TestAlone_3_1_0)|) & (|marking(TestIdentity_3_3_4)|!=|marking(TestAlone_3_3_4)|) & (|marking(TestIdentity_1_0_4)|!=|marking(TestAlone_1_0_4)|) & (|marking(TestIdentity_2_0_0)|!=|marking(TestAlone_2_0_0)|) & (|marking(TestIdentity_3_3_1)|!=|marking(TestAlone_3_3_1)|) & (|marking(TestIdentity_0_3_1)|!=|marking(TestAlone_0_3_1)|) & (|marking(TestIdentity_2_3_4)|!=|marking(TestAlone_2_3_4)|) & (|marking(TestIdentity_4_1_2)|!=|marking(TestAlone_4_1_2)|) & (|marking(TestIdentity_3_1_4)|!=|marking(TestAlone_3_1_4)|) & (|marking(TestIdentity_1_0_2)|!=|marking(TestAlone_1_0_2)|) & (|marking(TestIdentity_0_3_3)|!=|marking(TestAlone_0_3_3)|) & (|marking(TestIdentity_0_3_4)|!=|marking(TestAlone_0_3_4)|) & (|marking(TestIdentity_3_2_2)|!=|marking(TestAlone_3_2_2)|) & (|marking(TestIdentity_0_2_3)|!=|marking(TestAlone_0_2_3)|) & (|marking(TestIdentity_4_2_3)|!=|marking(TestAlone_4_2_3)|) & (|marking(TestIdentity_1_1_3)|!=|marking(TestAlone_1_1_3)|) & (|marking(TestIdentity_2_0_1)|!=|marking(TestAlone_2_0_1)|) & (|marking(TestIdentity_1_2_4)|!=|marking(TestAlone_1_2_4)|) & (|marking(TestIdentity_4_1_0)|!=|marking(TestAlone_4_1_0)|) & (|marking(TestIdentity_1_0_3)|!=|marking(TestAlone_1_0_3)|) & (|marking(TestIdentity_2_2_0)|!=|marking(TestAlone_2_2_0)|) & (|marking(TestIdentity_4_2_2)|!=|marking(TestAlone_4_2_2)|) & (|marking(TestIdentity_0_1_1)|!=|marking(TestAlone_0_1_1)|) & (|marking(TestIdentity_2_0_4)|!=|marking(TestAlone_2_0_4)|) & (|marking(TestIdentity_1_1_0)|!=|marking(TestAlone_1_1_0)|) & (|marking(TestIdentity_2_1_0)|!=|marking(TestAlone_2_1_0)|) & (|marking(TestIdentity_3_0_4)|!=|marking(TestAlone_3_0_4)|) & (|marking(TestIdentity_0_0_2)|!=|marking(TestAlone_0_0_2)|) & (|marking(TestIdentity_1_3_3)|!=|marking(TestAlone_1_3_3)|) & (|marking(TestIdentity_2_1_4)|!=|marking(TestAlone_2_1_4)|) & (|marking(TestIdentity_0_2_2)|!=|marking(TestAlone_0_2_2)|) & (|marking(TestIdentity_2_3_3)|!=|marking(TestAlone_2_3_3)|) & (|marking(TestIdentity_3_1_1)|!=|marking(TestAlone_3_1_1)|) & (|marking(TestIdentity_2_3_0)|!=|marking(TestAlone_2_3_0)|) & (|marking(TestIdentity_1_3_0)|!=|marking(TestAlone_1_3_0)|) & (|marking(TestIdentity_0_2_4)|!=|marking(TestAlone_0_2_4)|) & (|marking(TestIdentity_2_1_1)|!=|marking(TestAlone_2_1_1)|) & (|marking(TestIdentity_3_2_1)|!=|marking(TestAlone_3_2_1)|) & (|marking(TestIdentity_3_0_0)|!=|marking(TestAlone_3_0_0)|) & (|marking(TestIdentity_3_0_1)|!=|marking(TestAlone_3_0_1)|) & (|marking(TestIdentity_4_1_3)|!=|marking(TestAlone_4_1_3)|) & (|marking(TestIdentity_1_0_0)|!=|marking(TestAlone_1_0_0)|) & (|marking(TestIdentity_0_0_1)|!=|marking(TestAlone_0_0_1)|) & (|marking(TestIdentity_4_3_2)|!=|marking(TestAlone_4_3_2)|) & (|marking(TestIdentity_4_0_1)|!=|marking(TestAlone_4_0_1)|) & (|marking(TestIdentity_2_2_3)|!=|marking(TestAlone_2_2_3)|) & (|marking(TestIdentity_1_3_4)|!=|marking(TestAlone_1_3_4)|) & (|marking(TestIdentity_0_0_4)|!=|marking(TestAlone_0_0_4)|) & (|marking(TestIdentity_1_2_0)|!=|marking(TestAlone_1_2_0)|) & (|marking(TestIdentity_1_3_2)|!=|marking(TestAlone_1_3_2)|) & (|marking(TestIdentity_1_1_2)|!=|marking(TestAlone_1_1_2)|) & (|marking(TestIdentity_4_2_0)|!=|marking(TestAlone_4_2_0)|) & (|marking(TestIdentity_2_3_1)|!=|marking(TestAlone_2_3_1)|) & (|marking(TestIdentity_3_2_3)|!=0) & (|marking(TestIdentity_0_0_0)|!=0) & (|marking(TestIdentity_0_2_0)|!=0) & (|marking(TestIdentity_0_3_0)|!=0) & (|marking(TestIdentity_4_0_4)|!=0) & (|marking(TestIdentity_4_1_4)|!=0) & (|marking(TestIdentity_3_3_3)|!=0) & (|marking(TestIdentity_4_3_4)|!=0) & (|marking(TestIdentity_3_1_3)|!=0) & (|marking(TestIdentity_4_2_4)|!=0) & (|marking(TestIdentity_1_3_1)|!=0) & (|marking(TestIdentity_3_0_3)|!=0) & (|marking(TestIdentity_2_2_2)|!=0) & (|marking(TestIdentity_2_3_2)|!=0) & (|marking(TestIdentity_0_1_0)|!=0) & (|marking(TestIdentity_1_2_1)|!=0) & (|marking(TestIdentity_2_1_2)|!=0) & (|marking(TestIdentity_1_1_1)|!=0) & (|marking(TestIdentity_1_0_1)|!=0) & (|marking(TestIdentity_2_0_2)|!=0)) | ((true) & (true & (|marking(BeginLoop_1_3_1)|<=|marking(IsEndLoop_1_3_1)|) & (|marking(BeginLoop_4_1_3)|<=|marking(IsEndLoop_4_1_3)|) & (|marking(BeginLoop_1_0_1)|<=|marking(IsEndLoop_1_0_1)|) & (|marking(BeginLoop_0_2_4)|<=|marking(IsEndLoop_0_2_4)|) & (|marking(BeginLoop_0_0_0)|<=|marking(IsEndLoop_0_0_0)|) & (|marking(BeginLoop_2_1_2)|<=|marking(IsEndLoop_2_1_2)|) & (|marking(BeginLoop_0_1_3)|<=|marking(IsEndLoop_0_1_3)|) & (|marking(BeginLoop_1_2_0)|<=|marking(IsEndLoop_1_2_0)|) & (|marking(BeginLoop_0_3_3)|<=|marking(IsEndLoop_0_3_3)|) & (|marking(BeginLoop_4_0_1)|<=|marking(IsEndLoop_4_0_1)|) & (|marking(BeginLoop_4_1_1)|<=|marking(IsEndLoop_4_1_1)|) & (|marking(BeginLoop_4_1_0)|<=|marking(IsEndLoop_4_1_0)|) & (|marking(BeginLoop_3_1_1)|<=|marking(IsEndLoop_3_1_1)|) & (|marking(BeginLoop_1_1_2)|<=|marking(IsEndLoop_1_1_2)|) & (|marking(BeginLoop_0_1_0)|<=|marking(IsEndLoop_0_1_0)|) & (|marking(BeginLoop_3_1_2)|<=|marking(IsEndLoop_3_1_2)|) & (|marking(BeginLoop_1_2_2)|<=|marking(IsEndLoop_1_2_2)|) & (|marking(BeginLoop_0_3_0)|<=|marking(IsEndLoop_0_3_0)|) & (|marking(BeginLoop_2_2_0)|<=|marking(IsEndLoop_2_2_0)|) & (|marking(BeginLoop_4_0_2)|<=|marking(IsEndLoop_4_0_2)|) & (|marking(BeginLoop_1_2_4)|<=|marking(IsEndLoop_1_2_4)|) & (|marking(BeginLoop_2_1_1)|<=|marking(IsEndLoop_2_1_1)|) & (|marking(BeginLoop_1_3_3)|<=|marking(IsEndLoop_1_3_3)|) & (|marking(BeginLoop_4_3_4)|<=|marking(IsEndLoop_4_3_4)|) & (|marking(BeginLoop_3_3_2)|<=|marking(IsEndLoop_3_3_2)|) & (|marking(BeginLoop_4_1_4)|<=|marking(IsEndLoop_4_1_4)|) & (|marking(BeginLoop_2_0_4)|<=|marking(IsEndLoop_2_0_4)|) & (|marking(BeginLoop_1_3_0)|<=|marking(IsEndLoop_1_3_0)|) & (|marking(BeginLoop_0_1_2)|<=|marking(IsEndLoop_0_1_2)|) & (|marking(BeginLoop_0_1_1)|<=|marking(IsEndLoop_0_1_1)|) & (|marking(BeginLoop_4_2_4)|<=|marking(IsEndLoop_4_2_4)|) & (|marking(BeginLoop_1_0_0)|<=|marking(IsEndLoop_1_0_0)|) & (|marking(BeginLoop_0_2_2)|<=|marking(IsEndLoop_0_2_2)|) & (|marking(BeginLoop_2_2_4)|<=|marking(IsEndLoop_2_2_4)|) & (|marking(BeginLoop_3_3_1)|<=|marking(IsEndLoop_3_3_1)|) & (|marking(BeginLoop_2_3_2)|<=|marking(IsEndLoop_2_3_2)|) & (|marking(BeginLoop_4_2_0)|<=|marking(IsEndLoop_4_2_0)|) & (|marking(BeginLoop_1_3_4)|<=|marking(IsEndLoop_1_3_4)|) & (|marking(BeginLoop_4_2_2)|<=|marking(IsEndLoop_4_2_2)|) & (|marking(BeginLoop_2_0_3)|<=|marking(IsEndLoop_2_0_3)|) & (|marking(BeginLoop_0_2_1)|<=|marking(IsEndLoop_0_2_1)|) & (|marking(BeginLoop_3_1_4)|<=|marking(IsEndLoop_3_1_4)|) & (|marking(BeginLoop_4_1_2)|<=|marking(IsEndLoop_4_1_2)|) & (|marking(BeginLoop_3_2_4)|<=|marking(IsEndLoop_3_2_4)|) & (|marking(BeginLoop_3_2_2)|<=|marking(IsEndLoop_3_2_2)|) & (|marking(BeginLoop_2_0_2)|<=|marking(IsEndLoop_2_0_2)|) & (|marking(BeginLoop_3_3_3)|<=|marking(IsEndLoop_3_3_3)|) & (|marking(BeginLoop_0_3_2)|<=|marking(IsEndLoop_0_3_2)|) & (|marking(BeginLoop_2_2_2)|<=|marking(IsEndLoop_2_2_2)|) & (|marking(BeginLoop_2_3_3)|<=|marking(IsEndLoop_2_3_3)|) & (|marking(BeginLoop_4_3_0)|<=|marking(IsEndLoop_4_3_0)|) & (|marking(BeginLoop_4_2_3)|<=|marking(IsEndLoop_4_2_3)|) & (|marking(BeginLoop_4_0_3)|<=|marking(IsEndLoop_4_0_3)|) & (|marking(BeginLoop_2_1_4)|<=|marking(IsEndLoop_2_1_4)|) & (|marking(BeginLoop_3_2_1)|<=|marking(IsEndLoop_3_2_1)|) & (|marking(BeginLoop_2_0_0)|<=|marking(IsEndLoop_2_0_0)|) & (|marking(BeginLoop_4_0_4)|<=|marking(IsEndLoop_4_0_4)|) & (|marking(BeginLoop_1_1_0)|<=|marking(IsEndLoop_1_1_0)|) & (|marking(BeginLoop_3_3_0)|<=|marking(IsEndLoop_3_3_0)|) & (|marking(BeginLoop_1_1_3)|<=|marking(IsEndLoop_1_1_3)|) & (|marking(BeginLoop_0_0_3)|<=|marking(IsEndLoop_0_0_3)|) & (|marking(BeginLoop_3_0_3)|<=|marking(IsEndLoop_3_0_3)|) & (|marking(BeginLoop_3_2_3)|<=|marking(IsEndLoop_3_2_3)|) & (|marking(BeginLoop_2_3_0)|<=|marking(IsEndLoop_2_3_0)|) & (|marking(BeginLoop_1_1_1)|<=|marking(IsEndLoop_1_1_1)|) & (|marking(BeginLoop_0_0_1)|<=|marking(IsEndLoop_0_0_1)|) & (|marking(BeginLoop_3_0_2)|<=|marking(IsEndLoop_3_0_2)|) & (|marking(BeginLoop_4_3_1)|<=|marking(IsEndLoop_4_3_1)|) & (|marking(BeginLoop_2_1_0)|<=|marking(IsEndLoop_2_1_0)|) & (|marking(BeginLoop_3_1_3)|<=|marking(IsEndLoop_3_1_3)|) & (|marking(BeginLoop_1_0_4)|<=|marking(IsEndLoop_1_0_4)|) & (|marking(BeginLoop_3_0_0)|<=|marking(IsEndLoop_3_0_0)|) & (|marking(BeginLoop_2_2_1)|<=|marking(IsEndLoop_2_2_1)|) & (|marking(BeginLoop_1_2_1)|<=|marking(IsEndLoop_1_2_1)|) & (|marking(BeginLoop_2_3_1)|<=|marking(IsEndLoop_2_3_1)|) & (|marking(BeginLoop_1_1_4)|<=|marking(IsEndLoop_1_1_4)|) & (|marking(BeginLoop_1_0_3)|<=|marking(IsEndLoop_1_0_3)|) & (|marking(BeginLoop_3_0_4)|<=|marking(IsEndLoop_3_0_4)|) & (|marking(BeginLoop_1_0_2)|<=|marking(IsEndLoop_1_0_2)|) & (|marking(BeginLoop_3_1_0)|<=|marking(IsEndLoop_3_1_0)|) & (|marking(BeginLoop_4_3_3)|<=|marking(IsEndLoop_4_3_3)|) & (|marking(BeginLoop_3_3_4)|<=|marking(IsEndLoop_3_3_4)|) & (|marking(BeginLoop_2_1_3)|<=|marking(IsEndLoop_2_1_3)|) & (|marking(BeginLoop_0_3_1)|<=|marking(IsEndLoop_0_3_1)|) & (|marking(BeginLoop_4_2_1)|<=|marking(IsEndLoop_4_2_1)|) & (|marking(BeginLoop_3_2_0)|<=|marking(IsEndLoop_3_2_0)|) & (|marking(BeginLoop_0_0_2)|<=|marking(IsEndLoop_0_0_2)|) & (|marking(BeginLoop_1_3_2)|<=|marking(IsEndLoop_1_3_2)|) & (|marking(BeginLoop_2_3_4)|<=|marking(IsEndLoop_2_3_4)|) & (|marking(BeginLoop_2_2_3)|<=|marking(IsEndLoop_2_2_3)|) & (|marking(BeginLoop_0_0_4)|<=|marking(IsEndLoop_0_0_4)|) & (|marking(BeginLoop_0_3_4)|<=|marking(IsEndLoop_0_3_4)|) & (|marking(BeginLoop_0_2_0)|<=|marking(IsEndLoop_0_2_0)|) & (|marking(BeginLoop_0_1_4)|<=|marking(IsEndLoop_0_1_4)|) & (|marking(BeginLoop_2_0_1)|<=|marking(IsEndLoop_2_0_1)|) & (|marking(BeginLoop_0_2_3)|<=|marking(IsEndLoop_0_2_3)|) & (|marking(BeginLoop_4_3_2)|<=|marking(IsEndLoop_4_3_2)|) & (|marking(BeginLoop_1_2_3)|<=|marking(IsEndLoop_1_2_3)|) & (|marking(BeginLoop_3_0_1)|<=|marking(IsEndLoop_3_0_1)|) & (|marking(BeginLoop_4_0_0)|<=|marking(IsEndLoop_4_0_0)|))))
ctl p_1853_placecomparison_full_and_notx: E G (!(true & (|marking(TestIdentity_3_2_4)|!=|marking(TestAlone_3_2_4)|) & (|marking(TestIdentity_3_3_0)|!=|marking(TestAlone_3_3_0)|) & (|marking(TestIdentity_1_2_3)|!=|marking(TestAlone_1_2_3)|) & (|marking(TestIdentity_1_1_4)|!=|marking(TestAlone_1_1_4)|) & (|marking(TestIdentity_4_3_0)|!=|marking(TestAlone_4_3_0)|) & (|marking(TestIdentity_1_2_2)|!=|marking(TestAlone_1_2_2)|) & (|marking(TestIdentity_3_3_2)|!=|marking(TestAlone_3_3_2)|) & (|marking(TestIdentity_0_0_3)|!=|marking(TestAlone_0_0_3)|) & (|marking(TestIdentity_4_0_0)|!=|marking(TestAlone_4_0_0)|) & (|marking(TestIdentity_3_2_0)|!=|marking(TestAlone_3_2_0)|) & (|marking(TestIdentity_3_1_2)|!=|marking(TestAlone_3_1_2)|) & (|marking(TestIdentity_4_3_3)|!=|marking(TestAlone_4_3_3)|) & (|marking(TestIdentity_3_0_2)|!=|marking(TestAlone_3_0_2)|) & (|marking(TestIdentity_4_1_1)|!=|marking(TestAlone_4_1_1)|) & (|marking(TestIdentity_0_1_2)|!=|marking(TestAlone_0_1_2)|) & (|marking(TestIdentity_2_2_1)|!=|marking(TestAlone_2_2_1)|) & (|marking(TestIdentity_0_3_2)|!=|marking(TestAlone_0_3_2)|) & (|marking(TestIdentity_2_1_3)|!=|marking(TestAlone_2_1_3)|) & (|marking(TestIdentity_0_2_1)|!=|marking(TestAlone_0_2_1)|) & (|marking(TestIdentity_4_3_1)|!=|marking(TestAlone_4_3_1)|) & (|marking(TestIdentity_4_2_1)|!=|marking(TestAlone_4_2_1)|) & (|marking(TestIdentity_0_1_4)|!=|marking(TestAlone_0_1_4)|) & (|marking(TestIdentity_2_2_4)|!=|marking(TestAlone_2_2_4)|) & (|marking(TestIdentity_2_0_3)|!=|marking(TestAlone_2_0_3)|) & (|marking(TestIdentity_4_0_3)|!=|marking(TestAlone_4_0_3)|) & (|marking(TestIdentity_4_0_2)|!=|marking(TestAlone_4_0_2)|) & (|marking(TestIdentity_0_1_3)|!=|marking(TestAlone_0_1_3)|) & (|marking(TestIdentity_3_1_0)|!=|marking(TestAlone_3_1_0)|) & (|marking(TestIdentity_3_3_4)|!=|marking(TestAlone_3_3_4)|) & (|marking(TestIdentity_1_0_4)|!=|marking(TestAlone_1_0_4)|) & (|marking(TestIdentity_2_0_0)|!=|marking(TestAlone_2_0_0)|) & (|marking(TestIdentity_3_3_1)|!=|marking(TestAlone_3_3_1)|) & (|marking(TestIdentity_0_3_1)|!=|marking(TestAlone_0_3_1)|) & (|marking(TestIdentity_2_3_4)|!=|marking(TestAlone_2_3_4)|) & (|marking(TestIdentity_4_1_2)|!=|marking(TestAlone_4_1_2)|) & (|marking(TestIdentity_3_1_4)|!=|marking(TestAlone_3_1_4)|) & (|marking(TestIdentity_1_0_2)|!=|marking(TestAlone_1_0_2)|) & (|marking(TestIdentity_0_3_3)|!=|marking(TestAlone_0_3_3)|) & (|marking(TestIdentity_0_3_4)|!=|marking(TestAlone_0_3_4)|) & (|marking(TestIdentity_3_2_2)|!=|marking(TestAlone_3_2_2)|) & (|marking(TestIdentity_0_2_3)|!=|marking(TestAlone_0_2_3)|) & (|marking(TestIdentity_4_2_3)|!=|marking(TestAlone_4_2_3)|) & (|marking(TestIdentity_1_1_3)|!=|marking(TestAlone_1_1_3)|) & (|marking(TestIdentity_2_0_1)|!=|marking(TestAlone_2_0_1)|) & (|marking(TestIdentity_1_2_4)|!=|marking(TestAlone_1_2_4)|) & (|marking(TestIdentity_4_1_0)|!=|marking(TestAlone_4_1_0)|) & (|marking(TestIdentity_1_0_3)|!=|marking(TestAlone_1_0_3)|) & (|marking(TestIdentity_2_2_0)|!=|marking(TestAlone_2_2_0)|) & (|marking(TestIdentity_4_2_2)|!=|marking(TestAlone_4_2_2)|) & (|marking(TestIdentity_0_1_1)|!=|marking(TestAlone_0_1_1)|) & (|marking(TestIdentity_2_0_4)|!=|marking(TestAlone_2_0_4)|) & (|marking(TestIdentity_1_1_0)|!=|marking(TestAlone_1_1_0)|) & (|marking(TestIdentity_2_1_0)|!=|marking(TestAlone_2_1_0)|) & (|marking(TestIdentity_3_0_4)|!=|marking(TestAlone_3_0_4)|) & (|marking(TestIdentity_0_0_2)|!=|marking(TestAlone_0_0_2)|) & (|marking(TestIdentity_1_3_3)|!=|marking(TestAlone_1_3_3)|) & (|marking(TestIdentity_2_1_4)|!=|marking(TestAlone_2_1_4)|) & (|marking(TestIdentity_0_2_2)|!=|marking(TestAlone_0_2_2)|) & (|marking(TestIdentity_2_3_3)|!=|marking(TestAlone_2_3_3)|) & (|marking(TestIdentity_3_1_1)|!=|marking(TestAlone_3_1_1)|) & (|marking(TestIdentity_2_3_0)|!=|marking(TestAlone_2_3_0)|) & (|marking(TestIdentity_1_3_0)|!=|marking(TestAlone_1_3_0)|) & (|marking(TestIdentity_0_2_4)|!=|marking(TestAlone_0_2_4)|) & (|marking(TestIdentity_2_1_1)|!=|marking(TestAlone_2_1_1)|) & (|marking(TestIdentity_3_2_1)|!=|marking(TestAlone_3_2_1)|) & (|marking(TestIdentity_3_0_0)|!=|marking(TestAlone_3_0_0)|) & (|marking(TestIdentity_3_0_1)|!=|marking(TestAlone_3_0_1)|) & (|marking(TestIdentity_4_1_3)|!=|marking(TestAlone_4_1_3)|) & (|marking(TestIdentity_1_0_0)|!=|marking(TestAlone_1_0_0)|) & (|marking(TestIdentity_0_0_1)|!=|marking(TestAlone_0_0_1)|) & (|marking(TestIdentity_4_3_2)|!=|marking(TestAlone_4_3_2)|) & (|marking(TestIdentity_4_0_1)|!=|marking(TestAlone_4_0_1)|) & (|marking(TestIdentity_2_2_3)|!=|marking(TestAlone_2_2_3)|) & (|marking(TestIdentity_1_3_4)|!=|marking(TestAlone_1_3_4)|) & (|marking(TestIdentity_0_0_4)|!=|marking(TestAlone_0_0_4)|) & (|marking(TestIdentity_1_2_0)|!=|marking(TestAlone_1_2_0)|) & (|marking(TestIdentity_1_3_2)|!=|marking(TestAlone_1_3_2)|) & (|marking(TestIdentity_1_1_2)|!=|marking(TestAlone_1_1_2)|) & (|marking(TestIdentity_4_2_0)|!=|marking(TestAlone_4_2_0)|) & (|marking(TestIdentity_2_3_1)|!=|marking(TestAlone_2_3_1)|) & (|marking(TestIdentity_3_2_3)|!=0) & (|marking(TestIdentity_0_0_0)|!=0) & (|marking(TestIdentity_0_2_0)|!=0) & (|marking(TestIdentity_0_3_0)|!=0) & (|marking(TestIdentity_4_0_4)|!=0) & (|marking(TestIdentity_4_1_4)|!=0) & (|marking(TestIdentity_3_3_3)|!=0) & (|marking(TestIdentity_4_3_4)|!=0) & (|marking(TestIdentity_3_1_3)|!=0) & (|marking(TestIdentity_4_2_4)|!=0) & (|marking(TestIdentity_1_3_1)|!=0) & (|marking(TestIdentity_3_0_3)|!=0) & (|marking(TestIdentity_2_2_2)|!=0) & (|marking(TestIdentity_2_3_2)|!=0) & (|marking(TestIdentity_0_1_0)|!=0) & (|marking(TestIdentity_1_2_1)|!=0) & (|marking(TestIdentity_2_1_2)|!=0) & (|marking(TestIdentity_1_1_1)|!=0) & (|marking(TestIdentity_1_0_1)|!=0) & (|marking(TestIdentity_2_0_2)|!=0)) & ((true) & (true & (|marking(BeginLoop_1_3_1)|<=|marking(IsEndLoop_1_3_1)|) & (|marking(BeginLoop_4_1_3)|<=|marking(IsEndLoop_4_1_3)|) & (|marking(BeginLoop_1_0_1)|<=|marking(IsEndLoop_1_0_1)|) & (|marking(BeginLoop_0_2_4)|<=|marking(IsEndLoop_0_2_4)|) & (|marking(BeginLoop_0_0_0)|<=|marking(IsEndLoop_0_0_0)|) & (|marking(BeginLoop_2_1_2)|<=|marking(IsEndLoop_2_1_2)|) & (|marking(BeginLoop_0_1_3)|<=|marking(IsEndLoop_0_1_3)|) & (|marking(BeginLoop_1_2_0)|<=|marking(IsEndLoop_1_2_0)|) & (|marking(BeginLoop_0_3_3)|<=|marking(IsEndLoop_0_3_3)|) & (|marking(BeginLoop_4_0_1)|<=|marking(IsEndLoop_4_0_1)|) & (|marking(BeginLoop_4_1_1)|<=|marking(IsEndLoop_4_1_1)|) & (|marking(BeginLoop_4_1_0)|<=|marking(IsEndLoop_4_1_0)|) & (|marking(BeginLoop_3_1_1)|<=|marking(IsEndLoop_3_1_1)|) & (|marking(BeginLoop_1_1_2)|<=|marking(IsEndLoop_1_1_2)|) & (|marking(BeginLoop_0_1_0)|<=|marking(IsEndLoop_0_1_0)|) & (|marking(BeginLoop_3_1_2)|<=|marking(IsEndLoop_3_1_2)|) & (|marking(BeginLoop_1_2_2)|<=|marking(IsEndLoop_1_2_2)|) & (|marking(BeginLoop_0_3_0)|<=|marking(IsEndLoop_0_3_0)|) & (|marking(BeginLoop_2_2_0)|<=|marking(IsEndLoop_2_2_0)|) & (|marking(BeginLoop_4_0_2)|<=|marking(IsEndLoop_4_0_2)|) & (|marking(BeginLoop_1_2_4)|<=|marking(IsEndLoop_1_2_4)|) & (|marking(BeginLoop_2_1_1)|<=|marking(IsEndLoop_2_1_1)|) & (|marking(BeginLoop_1_3_3)|<=|marking(IsEndLoop_1_3_3)|) & (|marking(BeginLoop_4_3_4)|<=|marking(IsEndLoop_4_3_4)|) & (|marking(BeginLoop_3_3_2)|<=|marking(IsEndLoop_3_3_2)|) & (|marking(BeginLoop_4_1_4)|<=|marking(IsEndLoop_4_1_4)|) & (|marking(BeginLoop_2_0_4)|<=|marking(IsEndLoop_2_0_4)|) & (|marking(BeginLoop_1_3_0)|<=|marking(IsEndLoop_1_3_0)|) & (|marking(BeginLoop_0_1_2)|<=|marking(IsEndLoop_0_1_2)|) & (|marking(BeginLoop_0_1_1)|<=|marking(IsEndLoop_0_1_1)|) & (|marking(BeginLoop_4_2_4)|<=|marking(IsEndLoop_4_2_4)|) & (|marking(BeginLoop_1_0_0)|<=|marking(IsEndLoop_1_0_0)|) & (|marking(BeginLoop_0_2_2)|<=|marking(IsEndLoop_0_2_2)|) & (|marking(BeginLoop_2_2_4)|<=|marking(IsEndLoop_2_2_4)|) & (|marking(BeginLoop_3_3_1)|<=|marking(IsEndLoop_3_3_1)|) & (|marking(BeginLoop_2_3_2)|<=|marking(IsEndLoop_2_3_2)|) & (|marking(BeginLoop_4_2_0)|<=|marking(IsEndLoop_4_2_0)|) & (|marking(BeginLoop_1_3_4)|<=|marking(IsEndLoop_1_3_4)|) & (|marking(BeginLoop_4_2_2)|<=|marking(IsEndLoop_4_2_2)|) & (|marking(BeginLoop_2_0_3)|<=|marking(IsEndLoop_2_0_3)|) & (|marking(BeginLoop_0_2_1)|<=|marking(IsEndLoop_0_2_1)|) & (|marking(BeginLoop_3_1_4)|<=|marking(IsEndLoop_3_1_4)|) & (|marking(BeginLoop_4_1_2)|<=|marking(IsEndLoop_4_1_2)|) & (|marking(BeginLoop_3_2_4)|<=|marking(IsEndLoop_3_2_4)|) & (|marking(BeginLoop_3_2_2)|<=|marking(IsEndLoop_3_2_2)|) & (|marking(BeginLoop_2_0_2)|<=|marking(IsEndLoop_2_0_2)|) & (|marking(BeginLoop_3_3_3)|<=|marking(IsEndLoop_3_3_3)|) & (|marking(BeginLoop_0_3_2)|<=|marking(IsEndLoop_0_3_2)|) & (|marking(BeginLoop_2_2_2)|<=|marking(IsEndLoop_2_2_2)|) & (|marking(BeginLoop_2_3_3)|<=|marking(IsEndLoop_2_3_3)|) & (|marking(BeginLoop_4_3_0)|<=|marking(IsEndLoop_4_3_0)|) & (|marking(BeginLoop_4_2_3)|<=|marking(IsEndLoop_4_2_3)|) & (|marking(BeginLoop_4_0_3)|<=|marking(IsEndLoop_4_0_3)|) & (|marking(BeginLoop_2_1_4)|<=|marking(IsEndLoop_2_1_4)|) & (|marking(BeginLoop_3_2_1)|<=|marking(IsEndLoop_3_2_1)|) & (|marking(BeginLoop_2_0_0)|<=|marking(IsEndLoop_2_0_0)|) & (|marking(BeginLoop_4_0_4)|<=|marking(IsEndLoop_4_0_4)|) & (|marking(BeginLoop_1_1_0)|<=|marking(IsEndLoop_1_1_0)|) & (|marking(BeginLoop_3_3_0)|<=|marking(IsEndLoop_3_3_0)|) & (|marking(BeginLoop_1_1_3)|<=|marking(IsEndLoop_1_1_3)|) & (|marking(BeginLoop_0_0_3)|<=|marking(IsEndLoop_0_0_3)|) & (|marking(BeginLoop_3_0_3)|<=|marking(IsEndLoop_3_0_3)|) & (|marking(BeginLoop_3_2_3)|<=|marking(IsEndLoop_3_2_3)|) & (|marking(BeginLoop_2_3_0)|<=|marking(IsEndLoop_2_3_0)|) & (|marking(BeginLoop_1_1_1)|<=|marking(IsEndLoop_1_1_1)|) & (|marking(BeginLoop_0_0_1)|<=|marking(IsEndLoop_0_0_1)|) & (|marking(BeginLoop_3_0_2)|<=|marking(IsEndLoop_3_0_2)|) & (|marking(BeginLoop_4_3_1)|<=|marking(IsEndLoop_4_3_1)|) & (|marking(BeginLoop_2_1_0)|<=|marking(IsEndLoop_2_1_0)|) & (|marking(BeginLoop_3_1_3)|<=|marking(IsEndLoop_3_1_3)|) & (|marking(BeginLoop_1_0_4)|<=|marking(IsEndLoop_1_0_4)|) & (|marking(BeginLoop_3_0_0)|<=|marking(IsEndLoop_3_0_0)|) & (|marking(BeginLoop_2_2_1)|<=|marking(IsEndLoop_2_2_1)|) & (|marking(BeginLoop_1_2_1)|<=|marking(IsEndLoop_1_2_1)|) & (|marking(BeginLoop_2_3_1)|<=|marking(IsEndLoop_2_3_1)|) & (|marking(BeginLoop_1_1_4)|<=|marking(IsEndLoop_1_1_4)|) & (|marking(BeginLoop_1_0_3)|<=|marking(IsEndLoop_1_0_3)|) & (|marking(BeginLoop_3_0_4)|<=|marking(IsEndLoop_3_0_4)|) & (|marking(BeginLoop_1_0_2)|<=|marking(IsEndLoop_1_0_2)|) & (|marking(BeginLoop_3_1_0)|<=|marking(IsEndLoop_3_1_0)|) & (|marking(BeginLoop_4_3_3)|<=|marking(IsEndLoop_4_3_3)|) & (|marking(BeginLoop_3_3_4)|<=|marking(IsEndLoop_3_3_4)|) & (|marking(BeginLoop_2_1_3)|<=|marking(IsEndLoop_2_1_3)|) & (|marking(BeginLoop_0_3_1)|<=|marking(IsEndLoop_0_3_1)|) & (|marking(BeginLoop_4_2_1)|<=|marking(IsEndLoop_4_2_1)|) & (|marking(BeginLoop_3_2_0)|<=|marking(IsEndLoop_3_2_0)|) & (|marking(BeginLoop_0_0_2)|<=|marking(IsEndLoop_0_0_2)|) & (|marking(BeginLoop_1_3_2)|<=|marking(IsEndLoop_1_3_2)|) & (|marking(BeginLoop_2_3_4)|<=|marking(IsEndLoop_2_3_4)|) & (|marking(BeginLoop_2_2_3)|<=|marking(IsEndLoop_2_2_3)|) & (|marking(BeginLoop_0_0_4)|<=|marking(IsEndLoop_0_0_4)|) & (|marking(BeginLoop_0_3_4)|<=|marking(IsEndLoop_0_3_4)|) & (|marking(BeginLoop_0_2_0)|<=|marking(IsEndLoop_0_2_0)|) & (|marking(BeginLoop_0_1_4)|<=|marking(IsEndLoop_0_1_4)|) & (|marking(BeginLoop_2_0_1)|<=|marking(IsEndLoop_2_0_1)|) & (|marking(BeginLoop_0_2_3)|<=|marking(IsEndLoop_0_2_3)|) & (|marking(BeginLoop_4_3_2)|<=|marking(IsEndLoop_4_3_2)|) & (|marking(BeginLoop_1_2_3)|<=|marking(IsEndLoop_1_2_3)|) & (|marking(BeginLoop_3_0_1)|<=|marking(IsEndLoop_3_0_1)|) & (|marking(BeginLoop_4_0_0)|<=|marking(IsEndLoop_4_0_0)|))))


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