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

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

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

execution on node 31: cluster1u33.lip6.fr (runId=136966892301268_n_31)
=====================================================================
runnning marcie on Peterson-PT-3 (ReachabilityPlaceComparison)
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-3, examination is ReachabilityPlaceComparison
=====================================================================

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

START 1369682982

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=ReachabilityPlaceComparison.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 244 NrTr: 332)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m52sec


-> reachability set: #nodes 56076 (5.6e+04) #states 3,407,946 (6)



starting CTL model checker
--------------------------

checking: AG [[[[CS_2!=Idle_2 & [CS_3!=Idle_3 & [true & CS_0!=Idle_0]]] & CS_1!=Idle_1] & [CS_1=Idle_1 & [CS_2=Idle_2 & [[true & CS_0=Idle_0] & CS_3=Idle_3]]]]]
normalized: ~ [E [true U ~ [[[CS_1!=Idle_1 & [CS_2!=Idle_2 & [CS_3!=Idle_3 & [CS_0!=Idle_0 & true]]]] & [CS_1=Idle_1 & [CS_2=Idle_2 & [CS_3=Idle_3 & [CS_0=Idle_0 & true]]]]]]]]

-> the formula is FALSE

FORMULA p_7_placecomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m8sec

checking: AG [[[CS_1!=Idle_1 & [[[true & CS_0!=Idle_0] & CS_3!=Idle_3] & CS_2!=Idle_2]] | [[[CS_3=Idle_3 & [true & CS_0=Idle_0]] & CS_2=Idle_2] & CS_1=Idle_1]]]
normalized: ~ [E [true U ~ [[[CS_1!=Idle_1 & [CS_2!=Idle_2 & [CS_3!=Idle_3 & [CS_0!=Idle_0 & true]]]] | [CS_1=Idle_1 & [CS_2=Idle_2 & [CS_3=Idle_3 & [CS_0=Idle_0 & true]]]]]]]]

-> the formula is FALSE

FORMULA p_8_placecomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[true & CS_0=Idle_0] & CS_3=Idle_3] & CS_2=Idle_2] & CS_1=Idle_1] & [[CS_2!=Idle_2 & [[true & CS_0!=Idle_0] & CS_3!=Idle_3]] & CS_1!=Idle_1]]]
normalized: ~ [E [true U ~ [[[CS_1=Idle_1 & [CS_2=Idle_2 & [CS_3=Idle_3 & [CS_0=Idle_0 & true]]]] & [CS_1!=Idle_1 & [CS_2!=Idle_2 & [CS_3!=Idle_3 & [CS_0!=Idle_0 & true]]]]]]]]

-> the formula is FALSE

FORMULA p_9_placecomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[CS_1=Idle_1 & [[[CS_0=Idle_0 & true] & CS_3=Idle_3] & CS_2=Idle_2]] | [CS_1!=Idle_1 & [[[true & CS_0!=Idle_0] & CS_3!=Idle_3] & CS_2!=Idle_2]]]]
normalized: ~ [E [true U ~ [[[CS_1=Idle_1 & [CS_2=Idle_2 & [CS_3=Idle_3 & [CS_0=Idle_0 & true]]]] | [CS_1!=Idle_1 & [CS_2!=Idle_2 & [CS_3!=Idle_3 & [CS_0!=Idle_0 & true]]]]]]]]

-> the formula is FALSE

FORMULA p_10_placecomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[CS_1!=Idle_1 & [CS_2!=Idle_2 & [CS_3!=Idle_3 & [true & CS_0!=Idle_0]]]] | ~ [[CS_1=Idle_1 & [CS_2=Idle_2 & [[true & CS_0=Idle_0] & CS_3=Idle_3]]]]]]
normalized: ~ [E [true U ~ [[[CS_1!=Idle_1 & [CS_2!=Idle_2 & [CS_3!=Idle_3 & [CS_0!=Idle_0 & true]]]] | ~ [[CS_1=Idle_1 & [CS_2=Idle_2 & [CS_3=Idle_3 & [CS_0=Idle_0 & true]]]]]]]]]

-> the formula is TRUE

FORMULA p_11_placecomparison_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[false | [Idle_1>CS_1 | [[[Idle_0>CS_0 | false] | Idle_2>CS_2] | Idle_3>CS_3]]] & [true & [Idle_1>CS_1 & [Idle_3>CS_3 & [[true & Idle_0>CS_0] & Idle_2>CS_2]]]]] & [[IsEndLoop_2_0_2=0.000000000000000 & [[[[[IsEndLoop_2_2_2=0.000000000000000 & [[IsEndLoop_2_1_2=0.000000000000000 & [IsEndLoop_1_0_1=0.000000000000000 & [IsEndLoop_1_1_1=0.000000000000000 & [IsEndLoop_0_1_0=0.000000000000000 & [IsEndLoop_2_0_0=TestAlone_2_0_0 & [IsEndLoop_2_1_0=TestAlone_2_1_0 & [[IsEndLoop_1_1_0=TestAlone_1_1_0 & [IsEndLoop_3_0_0=TestAlone_3_0_0 & [[IsEndLoop_0_1_3=TestAlone_0_1_3 & [IsEndLoop_0_0_2=TestAlone_0_0_2 & [[IsEndLoop_0_2_1=TestAlone_0_2_1 & [[[IsEndLoop_3_2_0=TestAlone_3_2_0 & [IsEndLoop_2_0_1=TestAlone_2_0_1 & [[IsEndLoop_0_2_3=TestAlone_0_2_3 & [IsEndLoop_3_1_1=TestAlone_3_1_1 & [[[IsEndLoop_0_1_2=TestAlone_0_1_2 & [[[[[[IsEndLoop_0_0_1=TestAlone_0_0_1 & [[[[[[[[[[true & IsEndLoop_2_2_1=TestAlone_2_2_1] & IsEndLoop_1_1_3=TestAlone_1_1_3] & IsEndLoop_2_2_0=TestAlone_2_2_0] & IsEndLoop_3_0_1=TestAlone_3_0_1] & IsEndLoop_1_2_2=TestAlone_1_2_2] & IsEndLoop_1_0_0=TestAlone_1_0_0] & IsEndLoop_1_1_2=TestAlone_1_1_2] & IsEndLoop_0_2_2=TestAlone_0_2_2] & IsEndLoop_3_0_2=TestAlone_3_0_2] & IsEndLoop_1_0_2=TestAlone_1_0_2]] & IsEndLoop_2_2_3=TestAlone_2_2_3] & IsEndLoop_3_2_2=TestAlone_3_2_2] & IsEndLoop_1_2_3=TestAlone_1_2_3] & IsEndLoop_2_1_1=TestAlone_2_1_1] & IsEndLoop_1_2_0=TestAlone_1_2_0]] & IsEndLoop_1_0_3=TestAlone_1_0_3] & IsEndLoop_3_1_0=TestAlone_3_1_0]]] & IsEndLoop_0_0_3=TestAlone_0_0_3]]] & IsEndLoop_2_0_3=TestAlone_2_0_3] & IsEndLoop_0_1_1=TestAlone_0_1_1]] & IsEndLoop_3_2_1=TestAlone_3_2_1]]] & IsEndLoop_2_1_3=TestAlone_2_1_3]]] & IsEndLoop_3_1_2=TestAlone_3_1_2]]]]]]] & IsEndLoop_1_2_1=0.000000000000000]] & IsEndLoop_0_0_0=0.000000000000000] & IsEndLoop_3_1_3=0.000000000000000] & IsEndLoop_3_0_3=0.000000000000000] & IsEndLoop_3_2_3=0.000000000000000]] & IsEndLoop_0_2_0=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[[false | [[Idle_3>CS_3 | [Idle_2>CS_2 | [Idle_0>CS_0 | false]]] | Idle_1>CS_1]] & [[Idle_1>CS_1 & [Idle_3>CS_3 & [[true & Idle_0>CS_0] & Idle_2>CS_2]]] & true]] & [[IsEndLoop_2_0_2=0.000000000000000 & [[[[IsEndLoop_0_0_0=0.000000000000000 & [IsEndLoop_2_2_2=0.000000000000000 & [[[[[IsEndLoop_0_1_0=0.000000000000000 & [IsEndLoop_2_0_0=TestAlone_2_0_0 & [IsEndLoop_2_1_0=TestAlone_2_1_0 & [IsEndLoop_3_1_2=TestAlone_3_1_2 & [IsEndLoop_1_1_0=TestAlone_1_1_0 & [IsEndLoop_3_0_0=TestAlone_3_0_0 & [IsEndLoop_2_1_3=TestAlone_2_1_3 & [IsEndLoop_0_1_3=TestAlone_0_1_3 & [IsEndLoop_0_0_2=TestAlone_0_0_2 & [IsEndLoop_3_2_1=TestAlone_3_2_1 & [IsEndLoop_0_2_1=TestAlone_0_2_1 & [IsEndLoop_0_1_1=TestAlone_0_1_1 & [IsEndLoop_2_0_3=TestAlone_2_0_3 & [IsEndLoop_3_2_0=TestAlone_3_2_0 & [IsEndLoop_2_0_1=TestAlone_2_0_1 & [IsEndLoop_0_0_3=TestAlone_0_0_3 & [IsEndLoop_0_2_3=TestAlone_0_2_3 & [IsEndLoop_3_1_1=TestAlone_3_1_1 & [IsEndLoop_3_1_0=TestAlone_3_1_0 & [IsEndLoop_1_0_3=TestAlone_1_0_3 & [IsEndLoop_0_1_2=TestAlone_0_1_2 & [IsEndLoop_1_2_0=TestAlone_1_2_0 & [IsEndLoop_2_1_1=TestAlone_2_1_1 & [IsEndLoop_1_2_3=TestAlone_1_2_3 & [IsEndLoop_3_2_2=TestAlone_3_2_2 & [IsEndLoop_2_2_3=TestAlone_2_2_3 & [IsEndLoop_0_0_1=TestAlone_0_0_1 & [IsEndLoop_1_0_2=TestAlone_1_0_2 & [IsEndLoop_3_0_2=TestAlone_3_0_2 & [IsEndLoop_0_2_2=TestAlone_0_2_2 & [IsEndLoop_1_1_2=TestAlone_1_1_2 & [IsEndLoop_1_0_0=TestAlone_1_0_0 & [IsEndLoop_1_2_2=TestAlone_1_2_2 & [IsEndLoop_3_0_1=TestAlone_3_0_1 & [IsEndLoop_2_2_0=TestAlone_2_2_0 & [IsEndLoop_1_1_3=TestAlone_1_1_3 & [IsEndLoop_2_2_1=TestAlone_2_2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & IsEndLoop_1_1_1=0.000000000000000] & IsEndLoop_1_0_1=0.000000000000000] & IsEndLoop_2_1_2=0.000000000000000] & IsEndLoop_1_2_1=0.000000000000000]]] & IsEndLoop_3_1_3=0.000000000000000] & IsEndLoop_3_0_3=0.000000000000000] & IsEndLoop_3_2_3=0.000000000000000]] & IsEndLoop_0_2_0=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_12_placecomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[Idle_1>CS_1 & [Idle_3>CS_3 & [[true & Idle_0>CS_0] & Idle_2>CS_2]]] & true] & [false | [Idle_1>CS_1 | [[[Idle_0>CS_0 | false] | Idle_2>CS_2] | Idle_3>CS_3]]]] | [IsEndLoop_0_2_0=0.000000000000000 & [IsEndLoop_2_0_2=0.000000000000000 & [[IsEndLoop_3_0_3=0.000000000000000 & [IsEndLoop_3_1_3=0.000000000000000 & [IsEndLoop_0_0_0=0.000000000000000 & [IsEndLoop_2_2_2=0.000000000000000 & [[[IsEndLoop_1_0_1=0.000000000000000 & [[IsEndLoop_0_1_0=0.000000000000000 & [[IsEndLoop_2_1_0=TestAlone_2_1_0 & [[[[IsEndLoop_2_1_3=TestAlone_2_1_3 & [[[[[[[IsEndLoop_3_2_0=TestAlone_3_2_0 & [[IsEndLoop_0_0_3=TestAlone_0_0_3 & [[IsEndLoop_3_1_1=TestAlone_3_1_1 & [IsEndLoop_3_1_0=TestAlone_3_1_0 & [[IsEndLoop_0_1_2=TestAlone_0_1_2 & [[[[IsEndLoop_3_2_2=TestAlone_3_2_2 & [[[[IsEndLoop_3_0_2=TestAlone_3_0_2 & [[IsEndLoop_1_1_2=TestAlone_1_1_2 & [[[[[[IsEndLoop_2_2_1=TestAlone_2_2_1 & true] & IsEndLoop_1_1_3=TestAlone_1_1_3] & IsEndLoop_2_2_0=TestAlone_2_2_0] & IsEndLoop_3_0_1=TestAlone_3_0_1] & IsEndLoop_1_2_2=TestAlone_1_2_2] & IsEndLoop_1_0_0=TestAlone_1_0_0]] & IsEndLoop_0_2_2=TestAlone_0_2_2]] & IsEndLoop_1_0_2=TestAlone_1_0_2] & IsEndLoop_0_0_1=TestAlone_0_0_1] & IsEndLoop_2_2_3=TestAlone_2_2_3]] & IsEndLoop_1_2_3=TestAlone_1_2_3] & IsEndLoop_2_1_1=TestAlone_2_1_1] & IsEndLoop_1_2_0=TestAlone_1_2_0]] & IsEndLoop_1_0_3=TestAlone_1_0_3]]] & IsEndLoop_0_2_3=TestAlone_0_2_3]] & IsEndLoop_2_0_1=TestAlone_2_0_1]] & IsEndLoop_2_0_3=TestAlone_2_0_3] & IsEndLoop_0_1_1=TestAlone_0_1_1] & IsEndLoop_0_2_1=TestAlone_0_2_1] & IsEndLoop_3_2_1=TestAlone_3_2_1] & IsEndLoop_0_0_2=TestAlone_0_0_2] & IsEndLoop_0_1_3=TestAlone_0_1_3]] & IsEndLoop_3_0_0=TestAlone_3_0_0] & IsEndLoop_1_1_0=TestAlone_1_1_0] & IsEndLoop_3_1_2=TestAlone_3_1_2]] & IsEndLoop_2_0_0=TestAlone_2_0_0]] & IsEndLoop_1_1_1=0.000000000000000]] & IsEndLoop_2_1_2=0.000000000000000] & IsEndLoop_1_2_1=0.000000000000000]]]]] & IsEndLoop_3_2_3=0.000000000000000]]]]]
normalized: ~ [E [true U ~ [[[[true & [Idle_1>CS_1 & [Idle_3>CS_3 & [Idle_2>CS_2 & [true & Idle_0>CS_0]]]]] & [[Idle_1>CS_1 | [Idle_3>CS_3 | [[false | Idle_0>CS_0] | Idle_2>CS_2]]] | false]] | [[[IsEndLoop_3_2_3=0.000000000000000 & [IsEndLoop_3_0_3=0.000000000000000 & [[IsEndLoop_0_0_0=0.000000000000000 & [IsEndLoop_2_2_2=0.000000000000000 & [IsEndLoop_1_2_1=0.000000000000000 & [IsEndLoop_2_1_2=0.000000000000000 & [IsEndLoop_1_0_1=0.000000000000000 & [IsEndLoop_1_1_1=0.000000000000000 & [IsEndLoop_0_1_0=0.000000000000000 & [IsEndLoop_2_0_0=TestAlone_2_0_0 & [IsEndLoop_2_1_0=TestAlone_2_1_0 & [IsEndLoop_3_1_2=TestAlone_3_1_2 & [IsEndLoop_1_1_0=TestAlone_1_1_0 & [IsEndLoop_3_0_0=TestAlone_3_0_0 & [IsEndLoop_2_1_3=TestAlone_2_1_3 & [IsEndLoop_0_1_3=TestAlone_0_1_3 & [IsEndLoop_0_0_2=TestAlone_0_0_2 & [IsEndLoop_3_2_1=TestAlone_3_2_1 & [IsEndLoop_0_2_1=TestAlone_0_2_1 & [IsEndLoop_0_1_1=TestAlone_0_1_1 & [IsEndLoop_2_0_3=TestAlone_2_0_3 & [IsEndLoop_3_2_0=TestAlone_3_2_0 & [IsEndLoop_2_0_1=TestAlone_2_0_1 & [IsEndLoop_0_0_3=TestAlone_0_0_3 & [IsEndLoop_0_2_3=TestAlone_0_2_3 & [IsEndLoop_3_1_1=TestAlone_3_1_1 & [IsEndLoop_3_1_0=TestAlone_3_1_0 & [IsEndLoop_1_0_3=TestAlone_1_0_3 & [IsEndLoop_0_1_2=TestAlone_0_1_2 & [IsEndLoop_1_2_0=TestAlone_1_2_0 & [IsEndLoop_2_1_1=TestAlone_2_1_1 & [IsEndLoop_1_2_3=TestAlone_1_2_3 & [IsEndLoop_3_2_2=TestAlone_3_2_2 & [IsEndLoop_2_2_3=TestAlone_2_2_3 & [IsEndLoop_0_0_1=TestAlone_0_0_1 & [IsEndLoop_1_0_2=TestAlone_1_0_2 & [IsEndLoop_3_0_2=TestAlone_3_0_2 & [IsEndLoop_0_2_2=TestAlone_0_2_2 & [IsEndLoop_1_1_2=TestAlone_1_1_2 & [IsEndLoop_1_0_0=TestAlone_1_0_0 & [IsEndLoop_1_2_2=TestAlone_1_2_2 & [IsEndLoop_3_0_1=TestAlone_3_0_1 & [IsEndLoop_2_2_0=TestAlone_2_2_0 & [IsEndLoop_1_1_3=TestAlone_1_1_3 & [IsEndLoop_2_2_1=TestAlone_2_2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & IsEndLoop_3_1_3=0.000000000000000]]] & IsEndLoop_2_0_2=0.000000000000000] & IsEndLoop_0_2_0=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_13_placecomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[[Idle_3>CS_3 | [Idle_2>CS_2 | [false | Idle_0>CS_0]]] | Idle_1>CS_1] | false] & [true & [[[[true & Idle_0>CS_0] & Idle_2>CS_2] & Idle_3>CS_3] & Idle_1>CS_1]]] & [IsEndLoop_0_2_0=0.000000000000000 & [[[IsEndLoop_3_0_3=0.000000000000000 & [[[IsEndLoop_2_2_2=0.000000000000000 & [[IsEndLoop_2_1_2=0.000000000000000 & [[IsEndLoop_1_1_1=0.000000000000000 & [[[IsEndLoop_2_1_0=TestAlone_2_1_0 & [[[[IsEndLoop_2_1_3=TestAlone_2_1_3 & [[IsEndLoop_0_0_2=TestAlone_0_0_2 & [IsEndLoop_3_2_1=TestAlone_3_2_1 & [[IsEndLoop_0_1_1=TestAlone_0_1_1 & [[IsEndLoop_3_2_0=TestAlone_3_2_0 & [[[IsEndLoop_0_2_3=TestAlone_0_2_3 & [[[IsEndLoop_1_0_3=TestAlone_1_0_3 & [IsEndLoop_0_1_2=TestAlone_0_1_2 & [IsEndLoop_1_2_0=TestAlone_1_2_0 & [IsEndLoop_2_1_1=TestAlone_2_1_1 & [IsEndLoop_1_2_3=TestAlone_1_2_3 & [[[IsEndLoop_0_0_1=TestAlone_0_0_1 & [[[IsEndLoop_0_2_2=TestAlone_0_2_2 & [[[[IsEndLoop_3_0_1=TestAlone_3_0_1 & [[[true & IsEndLoop_2_2_1=TestAlone_2_2_1] & IsEndLoop_1_1_3=TestAlone_1_1_3] & IsEndLoop_2_2_0=TestAlone_2_2_0]] & IsEndLoop_1_2_2=TestAlone_1_2_2] & IsEndLoop_1_0_0=TestAlone_1_0_0] & IsEndLoop_1_1_2=TestAlone_1_1_2]] & IsEndLoop_3_0_2=TestAlone_3_0_2] & IsEndLoop_1_0_2=TestAlone_1_0_2]] & IsEndLoop_2_2_3=TestAlone_2_2_3] & IsEndLoop_3_2_2=TestAlone_3_2_2]]]]]] & IsEndLoop_3_1_0=TestAlone_3_1_0] & IsEndLoop_3_1_1=TestAlone_3_1_1]] & IsEndLoop_0_0_3=TestAlone_0_0_3] & IsEndLoop_2_0_1=TestAlone_2_0_1]] & IsEndLoop_2_0_3=TestAlone_2_0_3]] & IsEndLoop_0_2_1=TestAlone_0_2_1]]] & IsEndLoop_0_1_3=TestAlone_0_1_3]] & IsEndLoop_3_0_0=TestAlone_3_0_0] & IsEndLoop_1_1_0=TestAlone_1_1_0] & IsEndLoop_3_1_2=TestAlone_3_1_2]] & IsEndLoop_2_0_0=TestAlone_2_0_0] & IsEndLoop_0_1_0=0.000000000000000]] & IsEndLoop_1_0_1=0.000000000000000]] & IsEndLoop_1_2_1=0.000000000000000]] & IsEndLoop_0_0_0=0.000000000000000] & IsEndLoop_3_1_3=0.000000000000000]] & IsEndLoop_3_2_3=0.000000000000000] & IsEndLoop_2_0_2=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[IsEndLoop_0_2_0=0.000000000000000 & [IsEndLoop_2_0_2=0.000000000000000 & [IsEndLoop_3_2_3=0.000000000000000 & [IsEndLoop_3_0_3=0.000000000000000 & [IsEndLoop_3_1_3=0.000000000000000 & [IsEndLoop_0_0_0=0.000000000000000 & [IsEndLoop_2_2_2=0.000000000000000 & [IsEndLoop_1_2_1=0.000000000000000 & [IsEndLoop_2_1_2=0.000000000000000 & [IsEndLoop_1_0_1=0.000000000000000 & [IsEndLoop_1_1_1=0.000000000000000 & [IsEndLoop_0_1_0=0.000000000000000 & [IsEndLoop_2_0_0=TestAlone_2_0_0 & [IsEndLoop_2_1_0=TestAlone_2_1_0 & [IsEndLoop_3_1_2=TestAlone_3_1_2 & [IsEndLoop_1_1_0=TestAlone_1_1_0 & [IsEndLoop_3_0_0=TestAlone_3_0_0 & [IsEndLoop_2_1_3=TestAlone_2_1_3 & [IsEndLoop_0_1_3=TestAlone_0_1_3 & [IsEndLoop_0_0_2=TestAlone_0_0_2 & [IsEndLoop_3_2_1=TestAlone_3_2_1 & [IsEndLoop_0_2_1=TestAlone_0_2_1 & [IsEndLoop_0_1_1=TestAlone_0_1_1 & [IsEndLoop_2_0_3=TestAlone_2_0_3 & [IsEndLoop_3_2_0=TestAlone_3_2_0 & [IsEndLoop_2_0_1=TestAlone_2_0_1 & [IsEndLoop_0_0_3=TestAlone_0_0_3 & [IsEndLoop_0_2_3=TestAlone_0_2_3 & [IsEndLoop_3_1_1=TestAlone_3_1_1 & [IsEndLoop_3_1_0=TestAlone_3_1_0 & [IsEndLoop_1_0_3=TestAlone_1_0_3 & [IsEndLoop_0_1_2=TestAlone_0_1_2 & [IsEndLoop_1_2_0=TestAlone_1_2_0 & [IsEndLoop_2_1_1=TestAlone_2_1_1 & [IsEndLoop_1_2_3=TestAlone_1_2_3 & [IsEndLoop_3_2_2=TestAlone_3_2_2 & [IsEndLoop_2_2_3=TestAlone_2_2_3 & [IsEndLoop_0_0_1=TestAlone_0_0_1 & [IsEndLoop_1_0_2=TestAlone_1_0_2 & [IsEndLoop_3_0_2=TestAlone_3_0_2 & [IsEndLoop_0_2_2=TestAlone_0_2_2 & [[IsEndLoop_1_0_0=TestAlone_1_0_0 & [IsEndLoop_1_2_2=TestAlone_1_2_2 & [IsEndLoop_3_0_1=TestAlone_3_0_1 & [[IsEndLoop_1_1_3=TestAlone_1_1_3 & [IsEndLoop_2_2_1=TestAlone_2_2_1 & true]] & IsEndLoop_2_2_0=TestAlone_2_2_0]]]] & IsEndLoop_1_1_2=TestAlone_1_1_2]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[[Idle_1>CS_1 & [Idle_3>CS_3 & [Idle_2>CS_2 & [Idle_0>CS_0 & true]]]] & true] & [false | [Idle_1>CS_1 | [Idle_3>CS_3 | [Idle_2>CS_2 | [Idle_0>CS_0 | false]]]]]]]]]]

-> the formula is FALSE

FORMULA p_14_placecomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 1m19sec

STOP 1369683062

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


initing FirstDep: 0m0sec

633 1596 2359 3260 4030 4745 5395 5268 5363 5197 10231 10760 11988 12164 12339 13954 15752 17708 17776 18119 18284 20091 20351 20958 22021 22277 22184 22386 23588 23796 24542 24489 24569 24632 24528 25073 25474 26124 26152 26515 26970 26085 27293 26796 26505 27159 26730 26707 26663 26179 27117 26757 26824 26709 26489 27157 26575 26908 27001 27821 27297 27086 27011 29890 29301 29338 29416 29650 30098 30129 30044 31896 32095 32222 32095 35948 35529 35601 35435 35084 36613 37080 37460 37496 37015 37495 38594 39102 39547 40202 40108 40227 40240 40370 40099 40373 40039 39221 39582 39816 40126 39435 39297 39507 38191 39371 38666 38484 39001 38457 38357 38359 37889 38602 38229 38293 38385 38035 37253 40710 40353 41378 41282 41116 41863 41434 41411 41367 40877 44207 44349 45477 45872 46113 47887 48131 48671 48526 48426 48022 47947 47545 47293 47551 49400 50333 50800 50838 50744 50945 51697 51303 51296 51100 52698 52745 52547 52693 52478 51841 51432 51808 51627 51111 50660 49667 49397 48821 48632 48207 48353 47605 47123 47839 47316 46909 47560 47115 47091 47048 47501 47460 47087 47046 46870 46650 46124 50091 50167 50288 50286 50899 50672 51550 51471 51231 51239 51077 50739 52485 55138 55303 55904 58419 58246 58265 58197 57537 57346 58197 58317 58976 59198 59100 59502 59731 60464 61156 61167 60796 60910 61018 60733 62364 62295 62253 62218 62626 61365 61403 61248 61471 60764 60006 58111 58373 58413 57508 57312 57061 55940 56452 56105 55729 56183 55748 55824 55848 55417 56115 55775 55704 55877 55712 54777 55744
iterations count:256454 (772), effective:11356 (34)

initing FirstDep: 0m0sec


iterations count:332 (1), effective:0 (0)

iterations count:332 (1), effective:0 (0)

iterations count:332 (1), effective:0 (0)

iterations count:332 (1), effective:0 (0)

iterations count:332 (1), effective:0 (0)

iterations count:332 (1), effective:0 (0)

iterations count:332 (1), effective:0 (0)

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