Introduction
This page shows the outputs produced by the execution of marcie on NeoElection/3 (P/T). We provide:
- A short summary,
- the execution chart (evolution of CPU and memory over the execution),
- the sequence of actions to be executed by the VM,
- the results of these actions.
About the Execution
| Execution Summary | |||
| Memory (MB) | CPU (s) | End | |
| 800.78 | 9.20 | normal | |
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=NeoElection-PT-3
export BK_EXAMINATION=ReachabilityMarkingComparison
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/NeoElection-PT-3
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is NeoElection-PT-3, examination is ReachabilityMarkingComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh
Execution Outputs of marcie for NeoElection/3 (P/T)
This is useful if one wants to reexecute the tool in the VM from the submitted image disk.
execution on node 36: cluster1u38.lip6.fr (runId=136959876601507_n_36)
=====================================================================
runnning marcie on NeoElection-PT-3 (ReachabilityMarkingComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is NeoElection-PT-3, examination is ReachabilityMarkingComparison
=====================================================================
--------------------
content from stdout:
START 1369636168
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=ReachabilityMarkingComparison.txt
constant oo registered with value < INFINITY >
parse successfull!
(NrP: 972 NrTr: 1016)
net check time: 0m0sec
parse mcc successfull!
place and transition orderings generation:0m0sec
init dd package: 0m1sec
RS generation: 0m7sec
-> reachability set: #nodes 19347 (1.9e+04) #states 974,325 (5)
starting CTL model checker
--------------------------
checking: AG [[[[[[[masterList_3_1_0!=0.000000000000000 & [[masterList_0_1_0!=0.000000000000000 & [[masterList_2_1_1!=0.000000000000000 & [[masterList_2_1_2!=0.000000000000000 & [[masterList_0_2_2!=0.000000000000000 & [[masterList_3_3_3!=0.000000000000000 & [[masterList_3_2_0!=0.000000000000000 & [[masterList_2_1_3!=0.000000000000000 & [[masterList_0_1_3!=0.000000000000000 & [[masterList_1_1_3!=0.000000000000000 & [[masterList_2_2_2!=0.000000000000000 & [[masterList_0_1_2!=0.000000000000000 & [[masterList_3_1_1!=0.000000000000000 & [[masterList_2_2_0!=0.000000000000000 & [[masterList_3_3_2!=0.000000000000000 & [[masterList_2_3_0!=0.000000000000000 & [[masterList_3_2_1!=0.000000000000000 & [[masterList_2_3_2!=0.000000000000000 & [[masterList_2_3_1!=0.000000000000000 & [[masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [[masterList_1_3_0!=0.000000000000000 & [[true & 1.000000000000000!=masterList_0_2_1] & masterList_3_3_1!=0.000000000000000]] & masterList_1_2_0!=0.000000000000000]]] & masterList_3_1_2!=0.000000000000000]] & masterList_2_3_3!=0.000000000000000]] & masterList_0_3_0!=0.000000000000000]] & masterList_0_2_0!=0.000000000000000]] & masterList_0_2_3!=0.000000000000000]] & masterList_1_3_2!=0.000000000000000]] & masterList_3_1_3!=0.000000000000000]] & masterList_1_3_1!=0.000000000000000]] & masterList_2_1_0!=0.000000000000000]] & masterList_1_1_1!=0.000000000000000]] & masterList_0_3_3!=0.000000000000000]] & masterList_1_2_1!=0.000000000000000]] & masterList_3_3_0!=0.000000000000000]] & masterList_1_1_0!=0.000000000000000]] & masterList_1_2_3!=0.000000000000000]] & masterList_3_2_3!=0.000000000000000]] & masterList_2_2_1!=0.000000000000000]] & masterList_1_2_2!=0.000000000000000]] & masterList_1_1_2!=0.000000000000000]] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000] & [[masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [[masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [[[[[[[masterList_3_2_0!=0.000000000000000 & [[masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [[[[[masterList_2_1_0!=0.000000000000000 & [[[masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [[1.000000000000000!=masterList_1_3_3 & true] & masterList_0_2_1!=0.000000000000000]]]]]]]]]]]]]]]]]]]] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000]] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000]]]] & masterList_3_3_0!=0.000000000000000]] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000]]] & masterList_1_2_2!=0.000000000000000]]]]]] & masterList_2_2_3!=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [1.000000000000000!=masterList_0_2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_3_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
-> the formula is FALSE
FORMULA p_27_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m4sec
checking: AG [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [[[masterList_0_2_1!=0.000000000000000 & [true & 1.000000000000000!=masterList_1_3_3]] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [masterList_2_2_3!=0.000000000000000 & [[[masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [[masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [[masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [[masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [[[[[masterList_0_1_2!=0.000000000000000 & [[[masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [[[masterList_0_2_0!=0.000000000000000 & [[masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [[masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [1.000000000000000!=masterList_0_2_1 & true]]]]]]]] & masterList_2_3_3!=0.000000000000000]]] & masterList_3_2_1!=0.000000000000000]] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000]]]]] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000]] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000]]] & masterList_1_2_1!=0.000000000000000]]]]]]] & masterList_0_2_2!=0.000000000000000]]]]] & masterList_1_2_2!=0.000000000000000]]]]] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[[[[[[masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [[[[masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [[[[masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [[[masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [[[[[[[[[masterList_3_3_1!=0.000000000000000 & [1.000000000000000!=masterList_0_2_1 & true]] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000]]] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000]]]]]]]]]]]]]]] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000]]]] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000]]]]]]] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000] | [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=masterList_1_3_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000]]]]]]]]]]]]]]]]
-> the formula is FALSE
FORMULA p_28_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
checking: AG [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [[masterList_3_3_3!=0.000000000000000 & [[[[[masterList_1_2_1!=0.000000000000000 & [[[[[[[[[[masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [[masterList_3_3_2!=0.000000000000000 & [[[[[[[[[[masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [[[[[true & 1.000000000000000!=masterList_1_3_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000]]] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000]] & masterList_1_3_2!=0.000000000000000]]] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000]] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000]] & masterList_1_2_3!=0.000000000000000]]]]]]]]]]]]] & ~ [[[masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [[masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [[masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [[masterList_1_1_3!=0.000000000000000 & [[masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [[masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [1.000000000000000!=masterList_0_2_1 & true]]]]]]]]]]]] & masterList_0_2_0!=0.000000000000000]]]]]]]]]]]] & masterList_1_1_1!=0.000000000000000]] & masterList_0_3_3!=0.000000000000000]]]]]]]]]] & masterList_3_2_3!=0.000000000000000]]]]]]] & masterList_3_1_0!=0.000000000000000]]]] & masterList_2_2_3!=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[[[[[[masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [[[[[masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_3_3 & true]]]]]]]]]]]]]]]]]]]]]]]]] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000]]]]]]]]]]]]]]] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000] & ~ [[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [1.000000000000000!=masterList_0_2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
-> the formula is FALSE
FORMULA p_29_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
checking: AG [[[masterList_2_2_3!=0.000000000000000 & [[masterList_0_3_1!=0.000000000000000 & [[[[masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [[[masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [[masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [[masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [[masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [[masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [[masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [[masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [[masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_3_3 & true]]] & masterList_1_3_0!=0.000000000000000]]]]] & masterList_2_3_1!=0.000000000000000]]]]] & masterList_0_2_0!=0.000000000000000]]]]] & masterList_2_2_0!=0.000000000000000]]]]] & masterList_2_1_0!=0.000000000000000]]]]] & masterList_0_1_3!=0.000000000000000]]]]] & masterList_1_1_0!=0.000000000000000]]]]] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000]]] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000]] & masterList_0_3_2!=0.000000000000000]] | ~ [[[[[[[[[[[[[[[masterList_1_2_3!=0.000000000000000 & [[[[masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [[[[[[[[masterList_0_1_2!=0.000000000000000 & [[[[[[[[[masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [[[masterList_3_1_2!=0.000000000000000 & [[masterList_3_2_2!=0.000000000000000 & [[masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [true & 1.000000000000000!=masterList_0_2_1]]] & masterList_1_2_0!=0.000000000000000]] & masterList_0_1_1!=0.000000000000000]] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000]]]]] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000]] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000]]] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000]] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [masterList_2_3_3!=0.000000000000000 & [masterList_2_3_1!=0.000000000000000 & [masterList_3_1_2!=0.000000000000000 & [masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [masterList_3_3_1!=0.000000000000000 & [masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_3_3 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | ~ [[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [[[[[masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [[[[[masterList_0_1_1!=0.000000000000000 & [masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [[true & 1.000000000000000!=masterList_0_2_1] & masterList_3_3_1!=0.000000000000000]]]]] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000]]]]]]]]]]]]]]]]
-> the formula is TRUE
FORMULA p_30_markingcomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
checking: AG [[[[masterList_0_3_2!=0.000000000000000 & [[masterList_3_1_0!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [[[[[[[[[masterList_2_3_1!=0.000000000000000 & [[[[[[[[true & 1.000000000000000!=masterList_1_3_3] & masterList_0_2_1!=0.000000000000000] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000]] & masterList_2_3_3!=0.000000000000000] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000]]] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000]] & masterList_0_3_1!=0.000000000000000]] & masterList_2_2_3!=0.000000000000000] <-> [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [masterList_1_3_3!=0.000000000000000 & [masterList_3_1_0!=0.000000000000000 & [masterList_1_1_2!=0.000000000000000 & [masterList_0_1_0!=0.000000000000000 & [masterList_1_2_2!=0.000000000000000 & [masterList_2_1_1!=0.000000000000000 & [masterList_2_2_1!=0.000000000000000 & [masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [masterList_1_2_3!=0.000000000000000 & [masterList_3_3_3!=0.000000000000000 & [masterList_1_1_0!=0.000000000000000 & [masterList_3_2_0!=0.000000000000000 & [masterList_3_3_0!=0.000000000000000 & [masterList_2_1_3!=0.000000000000000 & [masterList_1_2_1!=0.000000000000000 & [masterList_0_1_3!=0.000000000000000 & [masterList_0_3_3!=0.000000000000000 & [masterList_1_1_3!=0.000000000000000 & [masterList_1_1_1!=0.000000000000000 & [masterList_2_2_2!=0.000000000000000 & [masterList_2_1_0!=0.000000000000000 & [masterList_0_1_2!=0.000000000000000 & [masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [masterList_2_2_0!=0.000000000000000 & [masterList_1_3_2!=0.000000000000000 & [masterList_3_3_2!=0.000000000000000 & [masterList_0_2_3!=0.000000000000000 & [masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [[[[masterList_2_3_3!=0.000000000000000 & [[[[masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [masterList_1_3_0!=0.000000000000000 & [[1.000000000000000!=masterList_0_2_1 & true] & masterList_3_3_1!=0.000000000000000]]]] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [[[[[[[[[masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_3_3 & true]] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000]]]]]] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000]]]] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000] & [masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [[[[[[[[[[masterList_2_3_3!=0.000000000000000 & [[[[masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [[[true & 1.000000000000000!=masterList_0_2_1] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000]]] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000]]]] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000]]]]] | [~ [[masterList_2_2_3!=0.000000000000000 & [masterList_0_3_2!=0.000000000000000 & [masterList_0_3_1!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[masterList_1_3_1!=0.000000000000000 & [masterList_3_1_1!=0.000000000000000 & [masterList_3_1_3!=0.000000000000000 & [[[[[[[[[[masterList_2_3_3!=0.000000000000000 & [[[[masterList_3_2_2!=0.000000000000000 & [masterList_1_2_0!=0.000000000000000 & [[[true & 1.000000000000000!=masterList_0_2_1] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000]]] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000]] & masterList_2_3_2!=0.000000000000000] & masterList_0_3_0!=0.000000000000000] & masterList_3_2_1!=0.000000000000000] & masterList_0_2_0!=0.000000000000000] & masterList_2_3_0!=0.000000000000000] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000]]]] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000] & masterList_0_2_2!=0.000000000000000] & masterList_3_2_3!=0.000000000000000] & masterList_2_1_2!=0.000000000000000] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_1_3_3!=0.000000000000000]]]]] & ~ [[[[[[[[[[[masterList_2_1_2!=0.000000000000000 & [masterList_3_2_3!=0.000000000000000 & [masterList_0_2_2!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[masterList_2_3_0!=0.000000000000000 & [masterList_0_2_0!=0.000000000000000 & [masterList_3_2_1!=0.000000000000000 & [masterList_0_3_0!=0.000000000000000 & [masterList_2_3_2!=0.000000000000000 & [[[[[[[[[masterList_0_2_1!=0.000000000000000 & [1.000000000000000!=masterList_1_3_3 & true]] & masterList_3_3_1!=0.000000000000000] & masterList_1_3_0!=0.000000000000000] & masterList_1_2_0!=0.000000000000000] & masterList_3_2_2!=0.000000000000000] & masterList_0_1_1!=0.000000000000000] & masterList_3_1_2!=0.000000000000000] & masterList_2_3_1!=0.000000000000000] & masterList_2_3_3!=0.000000000000000]]]]]] & masterList_0_2_3!=0.000000000000000] & masterList_3_3_2!=0.000000000000000] & masterList_1_3_2!=0.000000000000000] & masterList_2_2_0!=0.000000000000000] & masterList_3_1_3!=0.000000000000000] & masterList_3_1_1!=0.000000000000000] & masterList_1_3_1!=0.000000000000000] & masterList_0_1_2!=0.000000000000000] & masterList_2_1_0!=0.000000000000000] & masterList_2_2_2!=0.000000000000000] & masterList_1_1_1!=0.000000000000000] & masterList_1_1_3!=0.000000000000000] & masterList_0_3_3!=0.000000000000000] & masterList_0_1_3!=0.000000000000000] & masterList_1_2_1!=0.000000000000000] & masterList_2_1_3!=0.000000000000000] & masterList_3_3_0!=0.000000000000000] & masterList_3_2_0!=0.000000000000000] & masterList_1_1_0!=0.000000000000000] & masterList_3_3_3!=0.000000000000000] & masterList_1_2_3!=0.000000000000000]]]] & masterList_2_2_1!=0.000000000000000] & masterList_2_1_1!=0.000000000000000] & masterList_1_2_2!=0.000000000000000] & masterList_0_1_0!=0.000000000000000] & masterList_1_1_2!=0.000000000000000] & masterList_3_1_0!=0.000000000000000] & masterList_0_3_1!=0.000000000000000] & masterList_0_3_2!=0.000000000000000] & masterList_2_2_3!=0.000000000000000]]]]]]]
-> the formula is TRUE
FORMULA p_31_markingcomparison_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
checking: AG [[[masterList_2_2_3=0.000000000000000 & [masterList_0_3_2=0.000000000000000 & [masterList_0_3_1=0.000000000000000 & [masterList_1_3_3=0.000000000000000 & [masterList_3_1_0=0.000000000000000 & [masterList_1_1_2=0.000000000000000 & [masterList_0_1_0=0.000000000000000 & [masterList_1_2_2=0.000000000000000 & [masterList_2_1_1=0.000000000000000 & [masterList_2_2_1=0.000000000000000 & [masterList_2_1_2=0.000000000000000 & [masterList_3_2_3=0.000000000000000 & [masterList_0_2_2=0.000000000000000 & [masterList_1_2_3=0.000000000000000 & [masterList_3_3_3=0.000000000000000 & [masterList_1_1_0=0.000000000000000 & [masterList_3_2_0=0.000000000000000 & [masterList_3_3_0=0.000000000000000 & [masterList_2_1_3=0.000000000000000 & [masterList_1_2_1=0.000000000000000 & [masterList_0_1_3=0.000000000000000 & [masterList_0_3_3=0.000000000000000 & [masterList_1_1_3=0.000000000000000 & [masterList_1_1_1=0.000000000000000 & [masterList_2_2_2=0.000000000000000 & [masterList_2_1_0=0.000000000000000 & [masterList_0_1_2=0.000000000000000 & [masterList_1_3_1=0.000000000000000 & [masterList_3_1_1=0.000000000000000 & [masterList_3_1_3=0.000000000000000 & [masterList_2_2_0=0.000000000000000 & [masterList_1_3_2=0.000000000000000 & [masterList_3_3_2=0.000000000000000 & [masterList_0_2_3=0.000000000000000 & [masterList_2_3_0=0.000000000000000 & [masterList_0_2_0=0.000000000000000 & [masterList_3_2_1=0.000000000000000 & [masterList_2_3_2=0.000000000000000 & [masterList_2_3_3=0.000000000000000 & [masterList_2_3_1=0.000000000000000 & [masterList_3_1_2=0.000000000000000 & [masterList_0_1_1=0.000000000000000 & [masterList_3_2_2=0.000000000000000 & [masterList_1_2_0=0.000000000000000 & [masterList_1_3_0=0.000000000000000 & [masterList_3_3_1=0.000000000000000 & [masterList_0_2_1=0.000000000000000 & [1.000000000000000=masterList_0_3_0 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[[masterList_2_2_3!=0.000000000000000 | [masterList_0_3_2!=0.000000000000000 | [masterList_0_3_1!=0.000000000000000 | [masterList_1_3_3!=0.000000000000000 | [masterList_3_1_0!=0.000000000000000 | [masterList_1_1_2!=0.000000000000000 | [masterList_0_1_0!=0.000000000000000 | [masterList_1_2_2!=0.000000000000000 | [masterList_2_2_1!=0.000000000000000 | [masterList_2_1_2!=0.000000000000000 | [masterList_3_2_3!=0.000000000000000 | [masterList_0_2_2!=0.000000000000000 | [masterList_1_2_3!=0.000000000000000 | [masterList_3_3_3!=0.000000000000000 | [masterList_1_1_0!=0.000000000000000 | [masterList_3_2_0!=0.000000000000000 | [masterList_3_3_0!=0.000000000000000 | [masterList_2_1_3!=0.000000000000000 | [masterList_1_2_1!=0.000000000000000 | [masterList_0_1_3!=0.000000000000000 | [masterList_0_3_3!=0.000000000000000 | [masterList_1_1_3!=0.000000000000000 | [masterList_1_1_1!=0.000000000000000 | [masterList_2_2_2!=0.000000000000000 | [masterList_2_1_0!=0.000000000000000 | [masterList_0_1_2!=0.000000000000000 | [masterList_1_3_1!=0.000000000000000 | [masterList_3_1_1!=0.000000000000000 | [masterList_3_1_3!=0.000000000000000 | [masterList_2_2_0!=0.000000000000000 | [masterList_1_3_2!=0.000000000000000 | [masterList_3_3_2!=0.000000000000000 | [masterList_0_2_3!=0.000000000000000 | [masterList_2_3_0!=0.000000000000000 | [masterList_0_2_0!=0.000000000000000 | [masterList_3_2_1!=0.000000000000000 | [masterList_0_3_0!=0.000000000000000 | [masterList_2_3_2!=0.000000000000000 | [masterList_2_3_3!=0.000000000000000 | [masterList_2_3_1!=0.000000000000000 | [masterList_3_1_2!=0.000000000000000 | [masterList_0_1_1!=0.000000000000000 | [masterList_3_2_2!=0.000000000000000 | [masterList_1_2_0!=0.000000000000000 | [masterList_1_3_0!=0.000000000000000 | [masterList_3_3_1!=0.000000000000000 | [masterList_0_2_1!=0.000000000000000 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [1.000000000000000
-> the formula is FALSE
FORMULA p_32_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
checking: AG [[[masterList_2_2_3=0.000000000000000 & [masterList_0_3_2=0.000000000000000 & [masterList_0_3_1=0.000000000000000 & [[[[masterList_0_1_0=0.000000000000000 & [[[[[[[masterList_1_2_3=0.000000000000000 & [[[[masterList_3_3_0=0.000000000000000 & [[[[[masterList_1_1_3=0.000000000000000 & [[[[masterList_0_1_2=0.000000000000000 & [[masterList_3_1_1=0.000000000000000 & [[[[masterList_3_3_2=0.000000000000000 & [masterList_0_2_3=0.000000000000000 & [masterList_2_3_0=0.000000000000000 & [masterList_0_2_0=0.000000000000000 & [masterList_3_2_1=0.000000000000000 & [masterList_2_3_2=0.000000000000000 & [masterList_2_3_3=0.000000000000000 & [masterList_2_3_1=0.000000000000000 & [masterList_3_1_2=0.000000000000000 & [masterList_0_1_1=0.000000000000000 & [masterList_3_2_2=0.000000000000000 & [masterList_1_2_0=0.000000000000000 & [masterList_1_3_0=0.000000000000000 & [masterList_3_3_1=0.000000000000000 & [masterList_0_2_1=0.000000000000000 & [1.000000000000000=masterList_0_3_0 & true]]]]]]]]]]]]]]]] & masterList_1_3_2=0.000000000000000] & masterList_2_2_0=0.000000000000000] & masterList_3_1_3=0.000000000000000]] & masterList_1_3_1=0.000000000000000]] & masterList_2_1_0=0.000000000000000] & masterList_2_2_2=0.000000000000000] & masterList_1_1_1=0.000000000000000]] & masterList_0_3_3=0.000000000000000] & masterList_0_1_3=0.000000000000000] & masterList_1_2_1=0.000000000000000] & masterList_2_1_3=0.000000000000000]] & masterList_3_2_0=0.000000000000000] & masterList_1_1_0=0.000000000000000] & masterList_3_3_3=0.000000000000000]] & masterList_0_2_2=0.000000000000000] & masterList_3_2_3=0.000000000000000] & masterList_2_1_2=0.000000000000000] & masterList_2_2_1=0.000000000000000] & masterList_2_1_1=0.000000000000000] & masterList_1_2_2=0.000000000000000]] & masterList_1_1_2=0.000000000000000] & masterList_3_1_0=0.000000000000000] & masterList_1_3_3=0.000000000000000]]]] | [[[masterList_2_2_3!=0.000000000000000 | [masterList_0_3_2!=0.000000000000000 | [masterList_0_3_1!=0.000000000000000 | [masterList_1_3_3!=0.000000000000000 | [masterList_3_1_0!=0.000000000000000 | [masterList_1_1_2!=0.000000000000000 | [masterList_0_1_0!=0.000000000000000 | [masterList_1_2_2!=0.000000000000000 | [masterList_2_2_1!=0.000000000000000 | [masterList_2_1_2!=0.000000000000000 | [masterList_3_2_3!=0.000000000000000 | [masterList_0_2_2!=0.000000000000000 | [masterList_1_2_3!=0.000000000000000 | [masterList_3_3_3!=0.000000000000000 | [masterList_1_1_0!=0.000000000000000 | [masterList_3_2_0!=0.000000000000000 | [masterList_3_3_0!=0.000000000000000 | [masterList_2_1_3!=0.000000000000000 | [masterList_1_2_1!=0.000000000000000 | [masterList_0_1_3!=0.000000000000000 | [masterList_0_3_3!=0.000000000000000 | [masterList_1_1_3!=0.000000000000000 | [masterList_1_1_1!=0.000000000000000 | [masterList_2_2_2!=0.000000000000000 | [masterList_2_1_0!=0.000000000000000 | [masterList_0_1_2!=0.000000000000000 | [masterList_1_3_1!=0.000000000000000 | [masterList_3_1_1!=0.000000000000000 | [masterList_3_1_3!=0.000000000000000 | [masterList_2_2_0!=0.000000000000000 | [masterList_1_3_2!=0.000000000000000 | [masterList_3_3_2!=0.000000000000000 | [masterList_0_2_3!=0.000000000000000 | [masterList_2_3_0!=0.000000000000000 | [masterList_0_2_0!=0.000000000000000 | [masterList_3_2_1!=0.000000000000000 | [masterList_0_3_0!=0.000000000000000 | [masterList_2_3_2!=0.000000000000000 | [masterList_2_3_3!=0.000000000000000 | [masterList_2_3_1!=0.000000000000000 | [masterList_3_1_2!=0.000000000000000 | [masterList_0_1_1!=0.000000000000000 | [masterList_3_2_2!=0.000000000000000 | [masterList_1_2_0!=0.000000000000000 | [masterList_1_3_0!=0.000000000000000 | [masterList_3_3_1!=0.000000000000000 | [masterList_0_2_1!=0.000000000000000 | false]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [1.000000000000000
-> the formula is FALSE
FORMULA p_33_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
checking: AG [[[[[[masterList_1_3_3=0.000000000000000 & [[masterList_1_1_2=0.000000000000000 & [[[masterList_2_1_1=0.000000000000000 & [masterList_2_2_1=0.000000000000000 & [[[masterList_0_2_2=0.000000000000000 & [masterList_1_2_3=0.000000000000000 & [[masterList_1_1_0=0.000000000000000 & [[[masterList_2_1_3=0.000000000000000 & [[[masterList_0_3_3=0.000000000000000 & [masterList_1_1_3=0.000000000000000 & [masterList_1_1_1=0.000000000000000 & [masterList_2_2_2=0.000000000000000 & [masterList_2_1_0=0.000000000000000 & [masterList_0_1_2=0.000000000000000 & [masterList_1_3_1=0.000000000000000 & [masterList_3_1_1=0.000000000000000 & [masterList_3_1_3=0.000000000000000 & [masterList_2_2_0=0.000000000000000 & [masterList_1_3_2=0.000000000000000 & [masterList_3_3_2=0.000000000000000 & [masterList_0_2_3=0.000000000000000 & [masterList_2_3_0=0.000000000000000 & [masterList_0_2_0=0.000000000000000 & [masterList_3_2_1=0.000000000000000 & [masterList_2_3_2=0.000000000000000 & [masterList_2_3_3=0.000000000000000 & [masterList_2_3_1=0.000000000000000 & [[masterList_0_1_1=0.000000000000000 & [masterList_3_2_2=0.000000000000000 & [masterList_1_2_0=0.000000000000000 & [masterList_1_3_0=0.000000000000000 & [masterList_3_3_1=0.000000000000000 & [masterList_0_2_1=0.000000000000000 & [1.000000000000000=masterList_0_3_0 & true]]]]]]] & masterList_3_1_2=0.000000000000000]]]]]]]]]]]]]]]]]]]] & masterList_0_1_3=0.000000000000000] & masterList_1_2_1=0.000000000000000]] & masterList_3_3_0=0.000000000000000] & masterList_3_2_0=0.000000000000000]] & masterList_3_3_3=0.000000000000000]]] & masterList_3_2_3=0.000000000000000] & masterList_2_1_2=0.000000000000000]]] & masterList_1_2_2=0.000000000000000] & masterList_0_1_0=0.000000000000000]] & masterList_3_1_0=0.000000000000000]] & masterList_0_3_1=0.000000000000000] & masterList_0_3_2=0.000000000000000] & masterList_2_2_3=0.000000000000000] & [[true & [true & 1.000000000000000<=masterList_2_1_1]] & [[1.000000000000000
-> the formula is FALSE
FORMULA p_34_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS
mc time: 0m0sec
total processing time: 0m23sec
STOP 1369636192
--------------------
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
2413 2983 4406 5170 8021 8230 9312 9485 12146 12633 13261 15641 17360 19352
iterations count:14854 (14), effective:108 (0)
initing FirstDep: 0m0sec
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
19347
iterations count:1016 (1), effective:0 (0)
--------------------
content from /tmp/BenchKit_head_log_file.1659: