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

Execution Outputs of marcie for TokenRing/010 (P/T)

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

execution on node 27: cluster1u29.lip6.fr (runId=136989898601354_n_27)
=====================================================================
runnning marcie on TokenRing-PT-010 (CTLMarkingComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is TokenRing-PT-010, examination is CTLMarkingComparison
=====================================================================

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

START 1369909236

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 121 NrTr: 1111)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m2sec


-> reachability set: #nodes 6527 (6.5e+03) #states 58,905 (4)



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

checking: EF [[[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [[State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & [1.000000000000000=State_8_0 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_4_0=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [State_8_9!=0.000000000000000 & [State_2_9!=0.000000000000000 & [State_4_6!=0.000000000000000 & [State_5_0!=0.000000000000000 & [State_7_6!=0.000000000000000 & [State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [State_4_1!=0.000000000000000 & [State_4_9!=0.000000000000000 & [State_8_4!=0.000000000000000 & [State_1_2!=0.000000000000000 & [State_8_7!=0.000000000000000 & [State_0_2!=0.000000000000000 & [State_0_3!=0.000000000000000 & [State_2_2!=0.000000000000000 & [State_6_2!=0.000000000000000 & [State_9_6!=0.000000000000000 & [State_7_8!=0.000000000000000 & [State_6_1!=0.000000000000000 & [State_6_9!=0.000000000000000 & [State_0_4!=0.000000000000000 & [State_1_9!=0.000000000000000 & [State_4_2!=0.000000000000000 & [State_7_4!=0.000000000000000 & [State_2_7!=0.000000000000000 & [State_8_3!=0.000000000000000 & [State_3_1!=0.000000000000000 & [State_9_4!=0.000000000000000 & [State_0_5!=0.000000000000000 & [State_9_0!=0.000000000000000 & [State_4_0!=0.000000000000000 & [State_3_0!=0.000000000000000 & [State_8_2!=0.000000000000000 & [State_5_7!=0.000000000000000 & [State_6_3!=0.000000000000000 & [State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [State_6_7!=0.000000000000000 & [State_3_3!=0.000000000000000 & [State_4_8!=0.000000000000000 & [State_7_5!=0.000000000000000 & [State_1_4!=0.000000000000000 & [State_7_7!=0.000000000000000 & [State_5_1!=0.000000000000000 & [State_0_0!=0.000000000000000 & [State_9_9!=0.000000000000000 & [State_8_5!=0.000000000000000 & [State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [State_6_5!=0.000000000000000 & [State_1_5!=0.000000000000000 & [State_8_8!=0.000000000000000 & [State_2_1!=0.000000000000000 & [State_1_3!=0.000000000000000 & [State_3_9!=0.000000000000000 & [State_6_0!=0.000000000000000 & [State_1_6!=0.000000000000000 & [State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: E [true U [[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & [1.000000000000000=State_8_0 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [State_8_9!=0.000000000000000 & [State_2_9!=0.000000000000000 & [State_4_6!=0.000000000000000 & [State_5_0!=0.000000000000000 & [State_7_6!=0.000000000000000 & [State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [State_4_1!=0.000000000000000 & [State_4_9!=0.000000000000000 & [State_8_4!=0.000000000000000 & [State_1_2!=0.000000000000000 & [State_8_7!=0.000000000000000 & [State_0_2!=0.000000000000000 & [State_0_3!=0.000000000000000 & [State_2_2!=0.000000000000000 & [State_6_2!=0.000000000000000 & [State_9_6!=0.000000000000000 & [State_7_8!=0.000000000000000 & [State_6_1!=0.000000000000000 & [State_6_9!=0.000000000000000 & [State_0_4!=0.000000000000000 & [State_1_9!=0.000000000000000 & [State_4_2!=0.000000000000000 & [State_7_4!=0.000000000000000 & [State_2_7!=0.000000000000000 & [State_8_3!=0.000000000000000 & [State_3_1!=0.000000000000000 & [State_9_4!=0.000000000000000 & [State_0_5!=0.000000000000000 & [State_9_0!=0.000000000000000 & [State_4_0!=0.000000000000000 & [State_3_0!=0.000000000000000 & [State_8_2!=0.000000000000000 & [State_5_7!=0.000000000000000 & [State_6_3!=0.000000000000000 & [State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [State_6_7!=0.000000000000000 & [State_3_3!=0.000000000000000 & [State_4_8!=0.000000000000000 & [State_7_5!=0.000000000000000 & [State_1_4!=0.000000000000000 & [State_7_7!=0.000000000000000 & [State_5_1!=0.000000000000000 & [State_0_0!=0.000000000000000 & [State_9_9!=0.000000000000000 & [State_8_5!=0.000000000000000 & [State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [State_6_5!=0.000000000000000 & [State_1_5!=0.000000000000000 & [State_8_8!=0.000000000000000 & [State_2_1!=0.000000000000000 & [State_1_3!=0.000000000000000 & [State_3_9!=0.000000000000000 & [State_6_0!=0.000000000000000 & [State_1_6!=0.000000000000000 & [State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1046_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[State_2_9!=0.000000000000000 & [State_4_6!=0.000000000000000 & [[[[State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [[State_4_4!=0.000000000000000 & [[[[State_1_2!=0.000000000000000 & [[[[[State_6_2!=0.000000000000000 & [[[[[[[[State_7_4!=0.000000000000000 & [State_2_7!=0.000000000000000 & [State_8_3!=0.000000000000000 & [State_3_1!=0.000000000000000 & [State_9_4!=0.000000000000000 & [State_0_5!=0.000000000000000 & [[State_4_0!=0.000000000000000 & [State_3_0!=0.000000000000000 & [State_8_2!=0.000000000000000 & [[[State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [[[[[[State_7_7!=0.000000000000000 & [[[[[State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [[[[[State_1_3!=0.000000000000000 & [State_3_9!=0.000000000000000 & [State_6_0!=0.000000000000000 & [[[State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_7_0!=0.000000000000000] & State_1_6!=0.000000000000000]]]] & State_2_1!=0.000000000000000] & State_8_8!=0.000000000000000] & State_1_5!=0.000000000000000] & State_6_5!=0.000000000000000]]] & State_8_5!=0.000000000000000] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000] & State_5_1!=0.000000000000000]] & State_1_4!=0.000000000000000] & State_7_5!=0.000000000000000] & State_4_8!=0.000000000000000] & State_3_3!=0.000000000000000] & State_6_7!=0.000000000000000]]] & State_6_3!=0.000000000000000] & State_5_7!=0.000000000000000]]]] & State_9_0!=0.000000000000000]]]]]]] & State_4_2!=0.000000000000000] & State_1_9!=0.000000000000000] & State_0_4!=0.000000000000000] & State_6_9!=0.000000000000000] & State_6_1!=0.000000000000000] & State_7_8!=0.000000000000000] & State_9_6!=0.000000000000000]] & State_2_2!=0.000000000000000] & State_0_3!=0.000000000000000] & State_0_2!=0.000000000000000] & State_8_7!=0.000000000000000]] & State_8_4!=0.000000000000000] & State_4_9!=0.000000000000000] & State_4_1!=0.000000000000000]] & State_0_7!=0.000000000000000]]] & State_7_1!=0.000000000000000] & State_7_6!=0.000000000000000] & State_5_0!=0.000000000000000]]] & State_8_9!=0.000000000000000] | [[[[State_5_0=0.000000000000000 & [[State_7_1=0.000000000000000 & [[[[[State_4_1=0.000000000000000 & [[[[[[[[State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [[[[[State_3_6=0.000000000000000 & [[State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [[State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [[[[[[[[[[[State_7_7=0.000000000000000 & [[[[[[[State_6_5=0.000000000000000 & [[[[[State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [[State_8_1=0.000000000000000 & [[[State_5_5=0.000000000000000 & [[[[[[[State_5_4=0.000000000000000 & [[State_5_3=0.000000000000000 & [[[[State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [[State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [[State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & [true & 1.000000000000000=State_8_0]]] & State_2_3=0.000000000000000]]]] & State_3_5=0.000000000000000]]]]]]]]]]]]] & State_3_7=0.000000000000000] & State_1_7=0.000000000000000] & State_2_6=0.000000000000000]] & State_6_4=0.000000000000000]] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000] & State_9_5=0.000000000000000] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000]] & State_7_9=0.000000000000000] & State_9_2=0.000000000000000]] & State_9_1=0.000000000000000]]]]]] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000]] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000]] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000]]]]] & State_9_4=0.000000000000000]]]] & State_7_4=0.000000000000000]] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000] & State_0_4=0.000000000000000] & State_6_9=0.000000000000000]]]]] & State_2_2=0.000000000000000] & State_0_3=0.000000000000000] & State_0_2=0.000000000000000] & State_8_7=0.000000000000000] & State_1_2=0.000000000000000] & State_8_4=0.000000000000000] & State_4_9=0.000000000000000]] & State_4_4=0.000000000000000] & State_0_7=0.000000000000000] & State_0_8=0.000000000000000] & State_2_4=0.000000000000000]] & State_7_6=0.000000000000000]] & State_4_6=0.000000000000000] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[State_8_9!=0.000000000000000 & [State_2_9!=0.000000000000000 & [State_4_6!=0.000000000000000 & [State_5_0!=0.000000000000000 & [State_7_6!=0.000000000000000 & [State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [State_4_1!=0.000000000000000 & [State_4_9!=0.000000000000000 & [State_8_4!=0.000000000000000 & [State_1_2!=0.000000000000000 & [State_8_7!=0.000000000000000 & [State_0_2!=0.000000000000000 & [State_0_3!=0.000000000000000 & [State_2_2!=0.000000000000000 & [State_6_2!=0.000000000000000 & [State_9_6!=0.000000000000000 & [State_7_8!=0.000000000000000 & [State_6_1!=0.000000000000000 & [State_6_9!=0.000000000000000 & [State_0_4!=0.000000000000000 & [State_1_9!=0.000000000000000 & [State_4_2!=0.000000000000000 & [State_7_4!=0.000000000000000 & [State_2_7!=0.000000000000000 & [State_8_3!=0.000000000000000 & [State_3_1!=0.000000000000000 & [State_9_4!=0.000000000000000 & [State_0_5!=0.000000000000000 & [State_9_0!=0.000000000000000 & [State_4_0!=0.000000000000000 & [State_3_0!=0.000000000000000 & [State_8_2!=0.000000000000000 & [State_5_7!=0.000000000000000 & [State_6_3!=0.000000000000000 & [State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [State_6_7!=0.000000000000000 & [State_3_3!=0.000000000000000 & [State_4_8!=0.000000000000000 & [State_7_5!=0.000000000000000 & [State_1_4!=0.000000000000000 & [State_7_7!=0.000000000000000 & [State_5_1!=0.000000000000000 & [State_0_0!=0.000000000000000 & [State_9_9!=0.000000000000000 & [State_8_5!=0.000000000000000 & [State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [State_6_5!=0.000000000000000 & [State_1_5!=0.000000000000000 & [State_8_8!=0.000000000000000 & [State_2_1!=0.000000000000000 & [State_1_3!=0.000000000000000 & [State_3_9!=0.000000000000000 & [State_6_0!=0.000000000000000 & [State_1_6!=0.000000000000000 & [State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [[[[[[[[[[State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [[[State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & [1.000000000000000=State_8_0 & true]]]]]]]]]]]]]]]]]] & State_9_8=0.000000000000000] & State_0_1=0.000000000000000] & State_3_7=0.000000000000000] & State_1_7=0.000000000000000] & State_2_6=0.000000000000000] & State_5_3=0.000000000000000] & State_6_4=0.000000000000000] & State_5_4=0.000000000000000] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000] & State_9_5=0.000000000000000] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000] & State_5_5=0.000000000000000] & State_7_9=0.000000000000000] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000] & State_9_1=0.000000000000000]]]]]]]] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000]]]]]]]]]] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1047_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[[[[State_4_6=0.000000000000000 & [[[State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [[[State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [[[[[[State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [[[[State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [[State_3_3=0.000000000000000 & [[[[[State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [[State_8_8=0.000000000000000 & [[State_1_3=0.000000000000000 & [[[State_1_6=0.000000000000000 & [[[[State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [[State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [[State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [[State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [[State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [[[[[[State_2_8=0.000000000000000 & [[State_1_8=0.000000000000000 & [[[[[[[[[[[State_3_8=0.000000000000000 & [true & 1.000000000000000=State_8_0]] & State_8_6=0.000000000000000] & State_2_3=0.000000000000000] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000] & State_5_8=0.000000000000000] & State_0_9=0.000000000000000]] & State_4_7=0.000000000000000]] & State_6_6=0.000000000000000] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000] & State_0_1=0.000000000000000]]] & State_2_6=0.000000000000000]]] & State_5_4=0.000000000000000]]] & State_2_0=0.000000000000000]]]]] & State_7_9=0.000000000000000]]] & State_9_1=0.000000000000000] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000]] & State_6_0=0.000000000000000] & State_3_9=0.000000000000000]] & State_2_1=0.000000000000000]] & State_1_5=0.000000000000000]]]]]]]] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000]] & State_6_7=0.000000000000000]]]] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000]]]]] & State_3_1=0.000000000000000] & State_8_3=0.000000000000000] & State_2_7=0.000000000000000] & State_7_4=0.000000000000000] & State_3_6=0.000000000000000]]]]]]]]]]]]]]] & State_4_9=0.000000000000000] & State_4_1=0.000000000000000]]]]]] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000]] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000] & [State_8_9!=0.000000000000000 & [[[[State_7_6!=0.000000000000000 & [[State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [State_4_1!=0.000000000000000 & [State_4_9!=0.000000000000000 & [State_8_4!=0.000000000000000 & [State_1_2!=0.000000000000000 & [State_8_7!=0.000000000000000 & [State_0_2!=0.000000000000000 & [State_0_3!=0.000000000000000 & [State_2_2!=0.000000000000000 & [State_6_2!=0.000000000000000 & [State_9_6!=0.000000000000000 & [State_7_8!=0.000000000000000 & [State_6_1!=0.000000000000000 & [State_6_9!=0.000000000000000 & [State_0_4!=0.000000000000000 & [State_1_9!=0.000000000000000 & [State_4_2!=0.000000000000000 & [State_7_4!=0.000000000000000 & [State_2_7!=0.000000000000000 & [State_8_3!=0.000000000000000 & [State_3_1!=0.000000000000000 & [State_9_4!=0.000000000000000 & [State_0_5!=0.000000000000000 & [State_9_0!=0.000000000000000 & [State_4_0!=0.000000000000000 & [State_3_0!=0.000000000000000 & [State_8_2!=0.000000000000000 & [State_5_7!=0.000000000000000 & [State_6_3!=0.000000000000000 & [State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [[State_3_3!=0.000000000000000 & [[State_7_5!=0.000000000000000 & [[[State_5_1!=0.000000000000000 & [State_0_0!=0.000000000000000 & [State_9_9!=0.000000000000000 & [[State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [State_6_5!=0.000000000000000 & [State_1_5!=0.000000000000000 & [[[State_1_3!=0.000000000000000 & [[State_6_0!=0.000000000000000 & [[State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [[[[[[State_1_7!=0.000000000000000 & [[[[[[State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [[[State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [[[[[1.000000000000000!=State_3_6 & true] & State_3_8!=0.000000000000000] & State_8_6!=0.000000000000000] & State_2_3!=0.000000000000000] & State_0_6!=0.000000000000000]]]]]]]] & State_1_8!=0.000000000000000] & State_4_7!=0.000000000000000]]] & State_4_5!=0.000000000000000] & State_5_9!=0.000000000000000] & State_9_8!=0.000000000000000] & State_0_1!=0.000000000000000] & State_3_7!=0.000000000000000]] & State_2_6!=0.000000000000000] & State_5_3!=0.000000000000000] & State_6_4!=0.000000000000000] & State_8_0!=0.000000000000000] & State_5_4!=0.000000000000000]]]]]]]]]]]]]] & State_1_6!=0.000000000000000]] & State_3_9!=0.000000000000000]] & State_2_1!=0.000000000000000] & State_8_8!=0.000000000000000]]]]] & State_8_5!=0.000000000000000]]]] & State_7_7!=0.000000000000000] & State_1_4!=0.000000000000000]] & State_4_8!=0.000000000000000]] & State_6_7!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_7_1!=0.000000000000000]] & State_5_0!=0.000000000000000] & State_4_6!=0.000000000000000] & State_2_9!=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[[[State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [[[[State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [[State_7_8=0.000000000000000 & [[[[[[[[[[[[[[[[State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [[[[[State_5_1=0.000000000000000 & [[[[[[[[State_8_8=0.000000000000000 & [[[[[[[[State_9_1=0.000000000000000 & [[[State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=State_8_0] & State_3_8=0.000000000000000] & State_8_6=0.000000000000000] & State_2_3=0.000000000000000] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000] & State_5_8=0.000000000000000] & State_0_9=0.000000000000000] & State_1_8=0.000000000000000] & State_4_7=0.000000000000000] & State_2_8=0.000000000000000] & State_6_6=0.000000000000000] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000] & State_0_1=0.000000000000000] & State_3_7=0.000000000000000] & State_1_7=0.000000000000000] & State_2_6=0.000000000000000]]]]]]]]]]]] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000]] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000] & State_6_0=0.000000000000000] & State_3_9=0.000000000000000] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000]] & State_1_5=0.000000000000000] & State_6_5=0.000000000000000] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000]] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000]]]]]]]] & State_3_0=0.000000000000000] & State_4_0=0.000000000000000] & State_9_0=0.000000000000000] & State_0_5=0.000000000000000] & State_9_4=0.000000000000000] & State_3_1=0.000000000000000] & State_8_3=0.000000000000000] & State_2_7=0.000000000000000] & State_7_4=0.000000000000000] & State_3_6=0.000000000000000] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000] & State_0_4=0.000000000000000] & State_6_9=0.000000000000000] & State_6_1=0.000000000000000]] & State_9_6=0.000000000000000]]]]]]]]]] & State_4_4=0.000000000000000] & State_0_7=0.000000000000000] & State_0_8=0.000000000000000]]]]]] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000] & [[[[[[[[[[[[[[[[[[[[[[[[[[[State_7_4!=0.000000000000000 & [State_2_7!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_0_9!=0.000000000000000 & [[[[[[[State_0_6!=0.000000000000000 & [[State_8_6!=0.000000000000000 & [[1.000000000000000!=State_3_6 & true] & State_3_8!=0.000000000000000]] & State_2_3!=0.000000000000000]] & State_6_8!=0.000000000000000] & State_3_2!=0.000000000000000] & State_3_5!=0.000000000000000] & State_7_3!=0.000000000000000] & State_7_2!=0.000000000000000] & State_5_8!=0.000000000000000]] & State_1_8!=0.000000000000000] & State_4_7!=0.000000000000000] & State_2_8!=0.000000000000000] & State_6_6!=0.000000000000000] & State_4_5!=0.000000000000000] & State_5_9!=0.000000000000000] & State_9_8!=0.000000000000000] & State_0_1!=0.000000000000000] & State_3_7!=0.000000000000000] & State_1_7!=0.000000000000000] & State_2_6!=0.000000000000000] & State_5_3!=0.000000000000000] & State_6_4!=0.000000000000000] & State_8_0!=0.000000000000000] & State_5_4!=0.000000000000000] & State_3_4!=0.000000000000000] & State_4_3!=0.000000000000000] & State_2_0!=0.000000000000000] & State_9_5!=0.000000000000000] & State_5_2!=0.000000000000000] & State_5_6!=0.000000000000000] & State_5_5!=0.000000000000000] & State_7_9!=0.000000000000000] & State_9_2!=0.000000000000000] & State_8_1!=0.000000000000000] & State_9_1!=0.000000000000000] & State_1_1!=0.000000000000000] & State_7_0!=0.000000000000000] & State_1_6!=0.000000000000000] & State_6_0!=0.000000000000000] & State_3_9!=0.000000000000000] & State_1_3!=0.000000000000000] & State_2_1!=0.000000000000000] & State_8_8!=0.000000000000000] & State_1_5!=0.000000000000000] & State_6_5!=0.000000000000000] & State_9_7!=0.000000000000000] & State_1_0!=0.000000000000000] & State_8_5!=0.000000000000000] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000] & State_5_1!=0.000000000000000] & State_7_7!=0.000000000000000] & State_1_4!=0.000000000000000] & State_7_5!=0.000000000000000] & State_4_8!=0.000000000000000] & State_3_3!=0.000000000000000] & State_6_7!=0.000000000000000] & State_9_3!=0.000000000000000] & State_2_5!=0.000000000000000] & State_6_3!=0.000000000000000] & State_5_7!=0.000000000000000] & State_8_2!=0.000000000000000] & State_3_0!=0.000000000000000] & State_4_0!=0.000000000000000] & State_9_0!=0.000000000000000] & State_0_5!=0.000000000000000] & State_9_4!=0.000000000000000] & State_3_1!=0.000000000000000] & State_8_3!=0.000000000000000]]] & State_4_2!=0.000000000000000] & State_1_9!=0.000000000000000] & State_0_4!=0.000000000000000] & State_6_9!=0.000000000000000] & State_6_1!=0.000000000000000] & State_7_8!=0.000000000000000] & State_9_6!=0.000000000000000] & State_6_2!=0.000000000000000] & State_2_2!=0.000000000000000] & State_0_3!=0.000000000000000] & State_0_2!=0.000000000000000] & State_8_7!=0.000000000000000] & State_1_2!=0.000000000000000] & State_8_4!=0.000000000000000] & State_4_9!=0.000000000000000] & State_4_1!=0.000000000000000] & State_4_4!=0.000000000000000] & State_0_7!=0.000000000000000] & State_0_8!=0.000000000000000] & State_2_4!=0.000000000000000] & State_7_1!=0.000000000000000] & State_7_6!=0.000000000000000] & State_5_0!=0.000000000000000] & State_4_6!=0.000000000000000] & State_2_9!=0.000000000000000] & State_8_9!=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_1048_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[State_2_9!=0.000000000000000 & [[State_5_0!=0.000000000000000 & [[[State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [[[[State_1_2!=0.000000000000000 & [[[State_0_3!=0.000000000000000 & [[[[State_7_8!=0.000000000000000 & [[[State_0_4!=0.000000000000000 & [[State_4_2!=0.000000000000000 & [State_7_4!=0.000000000000000 & [[[[State_9_4!=0.000000000000000 & [State_0_5!=0.000000000000000 & [[State_4_0!=0.000000000000000 & [[State_8_2!=0.000000000000000 & [State_5_7!=0.000000000000000 & [State_6_3!=0.000000000000000 & [State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [State_6_7!=0.000000000000000 & [[[State_7_5!=0.000000000000000 & [State_1_4!=0.000000000000000 & [State_7_7!=0.000000000000000 & [State_5_1!=0.000000000000000 & [[State_9_9!=0.000000000000000 & [State_8_5!=0.000000000000000 & [State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [[[State_8_8!=0.000000000000000 & [State_2_1!=0.000000000000000 & [State_1_3!=0.000000000000000 & [[[[State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [[State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [[[State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [[[State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [[[[[State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [[[State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [[State_0_6!=0.000000000000000 & [[[State_3_8!=0.000000000000000 & [true & 1.000000000000000!=State_3_6]] & State_8_6!=0.000000000000000] & State_2_3!=0.000000000000000]] & State_6_8!=0.000000000000000]]]]]]] & State_1_8!=0.000000000000000] & State_4_7!=0.000000000000000]]]]] & State_9_8!=0.000000000000000] & State_0_1!=0.000000000000000] & State_3_7!=0.000000000000000] & State_1_7!=0.000000000000000]]]] & State_8_0!=0.000000000000000] & State_5_4!=0.000000000000000]]]]]] & State_5_6!=0.000000000000000] & State_5_5!=0.000000000000000]]] & State_8_1!=0.000000000000000]]]] & State_1_6!=0.000000000000000] & State_6_0!=0.000000000000000] & State_3_9!=0.000000000000000]]]] & State_1_5!=0.000000000000000] & State_6_5!=0.000000000000000]]]]] & State_0_0!=0.000000000000000]]]]] & State_4_8!=0.000000000000000] & State_3_3!=0.000000000000000]]]]]]] & State_3_0!=0.000000000000000]] & State_9_0!=0.000000000000000]]] & State_3_1!=0.000000000000000] & State_8_3!=0.000000000000000] & State_2_7!=0.000000000000000]]] & State_1_9!=0.000000000000000]] & State_6_9!=0.000000000000000] & State_6_1!=0.000000000000000]] & State_9_6!=0.000000000000000] & State_6_2!=0.000000000000000] & State_2_2!=0.000000000000000]] & State_0_2!=0.000000000000000] & State_8_7!=0.000000000000000]] & State_8_4!=0.000000000000000] & State_4_9!=0.000000000000000] & State_4_1!=0.000000000000000]]]]] & State_7_1!=0.000000000000000] & State_7_6!=0.000000000000000]] & State_4_6!=0.000000000000000]] & State_8_9!=0.000000000000000] | [State_8_9=0.000000000000000 & [[State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [[State_7_1=0.000000000000000 & [[State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [[State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [[[[[[[[[[[[State_1_9=0.000000000000000 & [[[State_7_4=0.000000000000000 & [[State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [[[[[[[[State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [[[State_7_5=0.000000000000000 & [[[State_5_1=0.000000000000000 & [[[[[[[State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [[State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [[State_1_6=0.000000000000000 & [[[State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [[State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & [true & 1.000000000000000=State_8_0]]]]]]]]]]]]]]]]]]]]]]]] & State_6_4=0.000000000000000]]]]]]]]]]]]] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000]] & State_6_0=0.000000000000000]]] & State_2_1=0.000000000000000]]] & State_6_5=0.000000000000000] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000]] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000]] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000]]] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000] & State_4_0=0.000000000000000] & State_9_0=0.000000000000000]]]]] & State_2_7=0.000000000000000]] & State_3_6=0.000000000000000] & State_4_2=0.000000000000000]] & State_0_4=0.000000000000000] & State_6_9=0.000000000000000] & State_6_1=0.000000000000000] & State_7_8=0.000000000000000] & State_9_6=0.000000000000000] & State_6_2=0.000000000000000] & State_2_2=0.000000000000000] & State_0_3=0.000000000000000] & State_0_2=0.000000000000000] & State_8_7=0.000000000000000] & State_1_2=0.000000000000000]]]] & State_4_4=0.000000000000000]]] & State_2_4=0.000000000000000]] & State_7_6=0.000000000000000]]] & State_2_9=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[[State_8_9!=0.000000000000000 & [State_2_9!=0.000000000000000 & [State_4_6!=0.000000000000000 & [State_5_0!=0.000000000000000 & [State_7_6!=0.000000000000000 & [State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [State_4_1!=0.000000000000000 & [State_4_9!=0.000000000000000 & [State_8_4!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_1_6!=0.000000000000000 & [State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_6_0!=0.000000000000000] & State_3_9!=0.000000000000000] & State_1_3!=0.000000000000000] & State_2_1!=0.000000000000000] & State_8_8!=0.000000000000000] & State_1_5!=0.000000000000000] & State_6_5!=0.000000000000000] & State_9_7!=0.000000000000000] & State_1_0!=0.000000000000000] & State_8_5!=0.000000000000000] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000] & State_5_1!=0.000000000000000] & State_7_7!=0.000000000000000] & State_1_4!=0.000000000000000] & State_7_5!=0.000000000000000] & State_4_8!=0.000000000000000] & State_3_3!=0.000000000000000] & State_6_7!=0.000000000000000] & State_9_3!=0.000000000000000] & State_2_5!=0.000000000000000] & State_6_3!=0.000000000000000] & State_5_7!=0.000000000000000] & State_8_2!=0.000000000000000] & State_3_0!=0.000000000000000] & State_4_0!=0.000000000000000] & State_9_0!=0.000000000000000] & State_0_5!=0.000000000000000] & State_9_4!=0.000000000000000] & State_3_1!=0.000000000000000] & State_8_3!=0.000000000000000] & State_2_7!=0.000000000000000] & State_7_4!=0.000000000000000] & State_4_2!=0.000000000000000] & State_1_9!=0.000000000000000] & State_0_4!=0.000000000000000] & State_6_9!=0.000000000000000] & State_6_1!=0.000000000000000] & State_7_8!=0.000000000000000] & State_9_6!=0.000000000000000] & State_6_2!=0.000000000000000] & State_2_2!=0.000000000000000] & State_0_3!=0.000000000000000] & State_0_2!=0.000000000000000] & State_8_7!=0.000000000000000] & State_1_2!=0.000000000000000]]]]]]]]]]]]]] | [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [[State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=State_8_0] & State_3_8=0.000000000000000] & State_8_6=0.000000000000000] & State_2_3=0.000000000000000] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000] & State_5_8=0.000000000000000] & State_0_9=0.000000000000000] & State_1_8=0.000000000000000] & State_4_7=0.000000000000000] & State_2_8=0.000000000000000] & State_6_6=0.000000000000000] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000] & State_0_1=0.000000000000000] & State_3_7=0.000000000000000]]] & State_5_3=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1049_markingcomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [A [[[[[[State_7_6!=0.000000000000000 & [State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [State_4_1!=0.000000000000000 & [[[[[State_0_2!=0.000000000000000 & [[[[State_9_6!=0.000000000000000 & [[State_6_1!=0.000000000000000 & [[[[[[[[State_3_1!=0.000000000000000 & [[[[[[[[[[State_9_3!=0.000000000000000 & [[[State_4_8!=0.000000000000000 & [[[[[[[[State_1_0!=0.000000000000000 & [State_9_7!=0.000000000000000 & [[State_1_5!=0.000000000000000 & [[[[[[[State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [[[State_7_9!=0.000000000000000 & [[State_5_6!=0.000000000000000 & [[[[[State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [[State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [[State_1_7!=0.000000000000000 & [[State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [[State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [[[[[State_7_3!=0.000000000000000 & [[[State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [[[[1.000000000000000!=State_3_6 & true] & State_3_8!=0.000000000000000] & State_8_6!=0.000000000000000] & State_2_3!=0.000000000000000]]] & State_3_2!=0.000000000000000] & State_3_5!=0.000000000000000]] & State_7_2!=0.000000000000000] & State_5_8!=0.000000000000000] & State_0_9!=0.000000000000000] & State_1_8!=0.000000000000000]]] & State_6_6!=0.000000000000000]]]]] & State_3_7!=0.000000000000000]] & State_2_6!=0.000000000000000]]] & State_8_0!=0.000000000000000]]] & State_4_3!=0.000000000000000] & State_2_0!=0.000000000000000] & State_9_5!=0.000000000000000] & State_5_2!=0.000000000000000]] & State_5_5!=0.000000000000000]] & State_9_2!=0.000000000000000] & State_8_1!=0.000000000000000]]]] & State_1_6!=0.000000000000000] & State_6_0!=0.000000000000000] & State_3_9!=0.000000000000000] & State_1_3!=0.000000000000000] & State_2_1!=0.000000000000000] & State_8_8!=0.000000000000000]] & State_6_5!=0.000000000000000]]] & State_8_5!=0.000000000000000] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000] & State_5_1!=0.000000000000000] & State_7_7!=0.000000000000000] & State_1_4!=0.000000000000000] & State_7_5!=0.000000000000000]] & State_3_3!=0.000000000000000] & State_6_7!=0.000000000000000]] & State_2_5!=0.000000000000000] & State_6_3!=0.000000000000000] & State_5_7!=0.000000000000000] & State_8_2!=0.000000000000000] & State_3_0!=0.000000000000000] & State_4_0!=0.000000000000000] & State_9_0!=0.000000000000000] & State_0_5!=0.000000000000000] & State_9_4!=0.000000000000000]] & State_8_3!=0.000000000000000] & State_2_7!=0.000000000000000] & State_7_4!=0.000000000000000] & State_4_2!=0.000000000000000] & State_1_9!=0.000000000000000] & State_0_4!=0.000000000000000] & State_6_9!=0.000000000000000]] & State_7_8!=0.000000000000000]] & State_6_2!=0.000000000000000] & State_2_2!=0.000000000000000] & State_0_3!=0.000000000000000]] & State_8_7!=0.000000000000000] & State_1_2!=0.000000000000000] & State_8_4!=0.000000000000000] & State_4_9!=0.000000000000000]]]]]]]] & State_5_0!=0.000000000000000] & State_4_6!=0.000000000000000] & State_2_9!=0.000000000000000] & State_8_9!=0.000000000000000] U ~ [[[State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [[[[[[State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [[State_4_9=0.000000000000000 & [[State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [[[State_3_6=0.000000000000000 & [[State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [[[[[State_4_0=0.000000000000000 & [[[[[[[[[State_4_8=0.000000000000000 & [[[[[[[[State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [[[State_1_3=0.000000000000000 & [[[State_1_6=0.000000000000000 & [[[State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [[State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [[[[State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [[State_1_8=0.000000000000000 & [[State_5_8=0.000000000000000 & [[[State_3_5=0.000000000000000 & [[State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [[true & 1.000000000000000=State_8_0] & State_3_8=0.000000000000000]]]]] & State_3_2=0.000000000000000]] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000]] & State_0_9=0.000000000000000]] & State_4_7=0.000000000000000]]] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000]]]]]]]]] & State_4_3=0.000000000000000]]]]]]]]]] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000]] & State_6_0=0.000000000000000] & State_3_9=0.000000000000000]] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000]]]]] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000]] & State_3_3=0.000000000000000] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000]] & State_9_0=0.000000000000000] & State_0_5=0.000000000000000] & State_9_4=0.000000000000000] & State_3_1=0.000000000000000]]] & State_7_4=0.000000000000000]] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000]]]]]]]]]]]] & State_8_4=0.000000000000000]] & State_4_1=0.000000000000000]]] & State_0_8=0.000000000000000] & State_2_4=0.000000000000000] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000]]] & State_8_9=0.000000000000000]]]]
normalized: ~ [E [true U ~ [[~ [EG [[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [[[State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [[true & 1.000000000000000=State_8_0] & State_3_8=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000] & State_9_5=0.000000000000000] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000] & State_5_5=0.000000000000000] & State_7_9=0.000000000000000] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000] & State_9_1=0.000000000000000] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000] & State_6_0=0.000000000000000] & State_3_9=0.000000000000000] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000] & State_6_5=0.000000000000000] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000]]]]]]] & ~ [E [~ [[[[State_4_6!=0.000000000000000 & [[[State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [State_6_7!=0.000000000000000 & [State_3_3!=0.000000000000000 & [State_4_8!=0.000000000000000 & [State_7_5!=0.000000000000000 & [State_1_4!=0.000000000000000 & [State_7_7!=0.000000000000000 & [State_5_1!=0.000000000000000 & [[[[[[[State_1_5!=0.000000000000000 & [State_8_8!=0.000000000000000 & [State_2_1!=0.000000000000000 & [State_1_3!=0.000000000000000 & [State_3_9!=0.000000000000000 & [State_6_0!=0.000000000000000 & [State_1_6!=0.000000000000000 & [State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_6_5!=0.000000000000000] & State_9_7!=0.000000000000000] & State_1_0!=0.000000000000000] & State_8_5!=0.000000000000000] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000]]]]]]]]]] & State_6_3!=0.000000000000000] & State_5_7!=0.000000000000000] & State_8_2!=0.000000000000000] & State_3_0!=0.000000000000000] & State_4_0!=0.000000000000000] & State_9_0!=0.000000000000000] & State_0_5!=0.000000000000000] & State_9_4!=0.000000000000000] & State_3_1!=0.000000000000000] & State_8_3!=0.000000000000000] & State_2_7!=0.000000000000000] & State_7_4!=0.000000000000000] & State_4_2!=0.000000000000000] & State_1_9!=0.000000000000000] & State_0_4!=0.000000000000000] & State_6_9!=0.000000000000000] & State_6_1!=0.000000000000000] & State_7_8!=0.000000000000000] & State_9_6!=0.000000000000000] & State_6_2!=0.000000000000000] & State_2_2!=0.000000000000000] & State_0_3!=0.000000000000000] & State_0_2!=0.000000000000000] & State_8_7!=0.000000000000000] & State_1_2!=0.000000000000000] & State_8_4!=0.000000000000000] & State_4_9!=0.000000000000000] & State_4_1!=0.000000000000000]]]]]] & State_7_6!=0.000000000000000] & State_5_0!=0.000000000000000]] & State_2_9!=0.000000000000000] & State_8_9!=0.000000000000000]] U [[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [[[State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_5_4=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [[true & 1.000000000000000=State_8_0] & State_3_8=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000] & State_9_5=0.000000000000000] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000] & State_5_5=0.000000000000000] & State_7_9=0.000000000000000] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000] & State_9_1=0.000000000000000] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000] & State_6_0=0.000000000000000] & State_3_9=0.000000000000000] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000] & State_6_5=0.000000000000000] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000]]]]] & ~ [[[[State_4_6!=0.000000000000000 & [[[State_7_1!=0.000000000000000 & [State_2_4!=0.000000000000000 & [State_0_8!=0.000000000000000 & [State_0_7!=0.000000000000000 & [State_4_4!=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_2_5!=0.000000000000000 & [State_9_3!=0.000000000000000 & [State_6_7!=0.000000000000000 & [State_3_3!=0.000000000000000 & [State_4_8!=0.000000000000000 & [State_7_5!=0.000000000000000 & [State_1_4!=0.000000000000000 & [State_7_7!=0.000000000000000 & [State_5_1!=0.000000000000000 & [[[[[[[State_1_5!=0.000000000000000 & [State_8_8!=0.000000000000000 & [State_2_1!=0.000000000000000 & [State_1_3!=0.000000000000000 & [State_3_9!=0.000000000000000 & [State_6_0!=0.000000000000000 & [State_1_6!=0.000000000000000 & [State_7_0!=0.000000000000000 & [State_1_1!=0.000000000000000 & [State_9_1!=0.000000000000000 & [State_8_1!=0.000000000000000 & [State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [State_5_5!=0.000000000000000 & [State_5_6!=0.000000000000000 & [State_5_2!=0.000000000000000 & [State_9_5!=0.000000000000000 & [State_2_0!=0.000000000000000 & [State_4_3!=0.000000000000000 & [State_3_4!=0.000000000000000 & [State_5_4!=0.000000000000000 & [State_8_0!=0.000000000000000 & [State_6_4!=0.000000000000000 & [State_5_3!=0.000000000000000 & [State_2_6!=0.000000000000000 & [State_1_7!=0.000000000000000 & [State_3_7!=0.000000000000000 & [State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [State_5_9!=0.000000000000000 & [State_4_5!=0.000000000000000 & [State_6_6!=0.000000000000000 & [State_2_8!=0.000000000000000 & [State_4_7!=0.000000000000000 & [State_1_8!=0.000000000000000 & [State_0_9!=0.000000000000000 & [State_5_8!=0.000000000000000 & [State_7_2!=0.000000000000000 & [State_7_3!=0.000000000000000 & [State_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [State_0_6!=0.000000000000000 & [State_2_3!=0.000000000000000 & [State_8_6!=0.000000000000000 & [State_3_8!=0.000000000000000 & [1.000000000000000!=State_3_6 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_6_5!=0.000000000000000] & State_9_7!=0.000000000000000] & State_1_0!=0.000000000000000] & State_8_5!=0.000000000000000] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000]]]]]]]]]] & State_6_3!=0.000000000000000] & State_5_7!=0.000000000000000] & State_8_2!=0.000000000000000] & State_3_0!=0.000000000000000] & State_4_0!=0.000000000000000] & State_9_0!=0.000000000000000] & State_0_5!=0.000000000000000] & State_9_4!=0.000000000000000] & State_3_1!=0.000000000000000] & State_8_3!=0.000000000000000] & State_2_7!=0.000000000000000] & State_7_4!=0.000000000000000] & State_4_2!=0.000000000000000] & State_1_9!=0.000000000000000] & State_0_4!=0.000000000000000] & State_6_9!=0.000000000000000] & State_6_1!=0.000000000000000] & State_7_8!=0.000000000000000] & State_9_6!=0.000000000000000] & State_6_2!=0.000000000000000] & State_2_2!=0.000000000000000] & State_0_3!=0.000000000000000] & State_0_2!=0.000000000000000] & State_8_7!=0.000000000000000] & State_1_2!=0.000000000000000] & State_8_4!=0.000000000000000] & State_4_9!=0.000000000000000] & State_4_1!=0.000000000000000]]]]]] & State_7_6!=0.000000000000000] & State_5_0!=0.000000000000000]] & State_2_9!=0.000000000000000] & State_8_9!=0.000000000000000]]]]]]]]]

.
EG iterations: 1
-> the formula is TRUE

FORMULA p_1050_markingcomparison_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[[[State_4_6=0.000000000000000 & [[[State_7_1=0.000000000000000 & [[State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [[State_4_1=0.000000000000000 & [[State_8_4=0.000000000000000 & [[State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [[[State_6_2=0.000000000000000 & [[State_7_8=0.000000000000000 & [[State_6_9=0.000000000000000 & [[[[State_3_6=0.000000000000000 & [[State_2_7=0.000000000000000 & [[[[State_0_5=0.000000000000000 & [[State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [[State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [[State_9_3=0.000000000000000 & [[State_3_3=0.000000000000000 & [[[[[State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [[State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [[State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [[State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [[State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [[State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [[State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [[State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [[State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [true & State_3_8=0.000000000000000]]]] & State_6_8=0.000000000000000]]]]]] & State_0_9=0.000000000000000]]]]]] & State_5_9=0.000000000000000]]]]]] & State_5_3=0.000000000000000]]]]]] & State_2_0=0.000000000000000]]]]]] & State_9_2=0.000000000000000]]]]]] & State_3_9=0.000000000000000]]]]]] & State_9_7=0.000000000000000]]]]]] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000]] & State_6_7=0.000000000000000]] & State_2_5=0.000000000000000]]] & State_8_2=0.000000000000000]]] & State_9_0=0.000000000000000]] & State_9_4=0.000000000000000] & State_3_1=0.000000000000000] & State_8_3=0.000000000000000]] & State_7_4=0.000000000000000]] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000] & State_0_4=0.000000000000000]] & State_6_1=0.000000000000000]] & State_9_6=0.000000000000000]] & State_2_2=0.000000000000000] & State_0_3=0.000000000000000]]] & State_1_2=0.000000000000000]] & State_4_9=0.000000000000000]] & State_4_4=0.000000000000000]]] & State_2_4=0.000000000000000]] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000]] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000] & [true & 1.000000000000000>State_6_0]] & [[[[State_2_9=0.000000000000000 & [[[[[[[[State_4_4=0.000000000000000 & [[[[[[State_0_2=0.000000000000000 & [[[[State_9_6=0.000000000000000 & [[[[State_0_4=0.000000000000000 & [[[[State_7_4=0.000000000000000 & [[[[State_9_4=0.000000000000000 & [[[[[[[[State_2_5=0.000000000000000 & [[State_6_7=0.000000000000000 & [[State_4_8=0.000000000000000 & [[State_1_4=0.000000000000000 & [[State_5_1=0.000000000000000 & [[[[State_1_0=0.000000000000000 & [[State_6_5=0.000000000000000 & [[State_8_8=0.000000000000000 & [[[[State_6_0=0.000000000000000 & [[[[[[State_7_9=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[State_1_8=0.000000000000000 & [[[[[[[[[State_2_3=0.000000000000000 & [[true & State_3_8=0.000000000000000] & State_8_6=0.000000000000000]] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000] & State_5_8=0.000000000000000] & State_0_9=0.000000000000000]] & State_4_7=0.000000000000000] & State_2_8=0.000000000000000] & State_6_6=0.000000000000000] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000] & State_0_1=0.000000000000000] & State_3_7=0.000000000000000] & State_1_7=0.000000000000000] & State_2_6=0.000000000000000] & State_5_3=0.000000000000000] & State_6_4=0.000000000000000] & State_8_0=0.000000000000000] & State_5_4=0.000000000000000] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000] & State_9_5=0.000000000000000] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000] & State_5_5=0.000000000000000]] & State_9_2=0.000000000000000] & State_9_1=0.000000000000000] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000]] & State_3_9=0.000000000000000] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000]] & State_1_5=0.000000000000000]] & State_9_7=0.000000000000000]] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000]] & State_7_7=0.000000000000000]] & State_7_5=0.000000000000000]] & State_3_3=0.000000000000000]] & State_9_3=0.000000000000000]] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000] & State_4_0=0.000000000000000] & State_9_0=0.000000000000000] & State_0_5=0.000000000000000]] & State_3_1=0.000000000000000] & State_8_3=0.000000000000000] & State_2_7=0.000000000000000]] & State_3_6=0.000000000000000] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000]] & State_6_9=0.000000000000000] & State_6_1=0.000000000000000] & State_7_8=0.000000000000000]] & State_6_2=0.000000000000000] & State_2_2=0.000000000000000] & State_0_3=0.000000000000000]] & State_8_7=0.000000000000000] & State_1_2=0.000000000000000] & State_8_4=0.000000000000000] & State_4_9=0.000000000000000] & State_4_1=0.000000000000000]] & State_0_7=0.000000000000000] & State_0_8=0.000000000000000] & State_2_4=0.000000000000000] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000] & State_4_6=0.000000000000000]] & State_8_9=0.000000000000000] & [true & 1.000000000000000>State_8_1]] & [[false | 1.000000000000000>State_8_1] | false]]]]
normalized: E [true U [[[false | [1.000000000000000>State_8_1 | false]] & [[1.000000000000000>State_8_1 & true] & [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[1.000000000000000>State_6_0 & true] & [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1051_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[[[1.000000000000000>State_8_1 | false] | false] & [[1.000000000000000>State_8_1 & true] & [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [[State_5_0=0.000000000000000 & [[State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [[[[State_0_2=0.000000000000000 & [[[State_6_2=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[State_6_0=0.000000000000000 & [[[[[[State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [[State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [[State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [[[[[[[[State_3_5=0.000000000000000 & [[[[State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=0.000000000000000]] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000] & State_5_8=0.000000000000000] & State_0_9=0.000000000000000] & State_1_8=0.000000000000000] & State_4_7=0.000000000000000] & State_2_8=0.000000000000000]]]] & State_9_8=0.000000000000000]]]]]]]]] & State_3_4=0.000000000000000]]]]]]]] & State_9_2=0.000000000000000] & State_9_1=0.000000000000000] & State_1_1=0.000000000000000] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000]] & State_3_9=0.000000000000000] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000] & State_6_5=0.000000000000000] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000] & State_4_0=0.000000000000000] & State_9_0=0.000000000000000] & State_0_5=0.000000000000000] & State_9_4=0.000000000000000] & State_3_1=0.000000000000000] & State_8_3=0.000000000000000] & State_2_7=0.000000000000000] & State_7_4=0.000000000000000] & State_3_6=0.000000000000000] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000] & State_0_4=0.000000000000000] & State_6_9=0.000000000000000] & State_6_1=0.000000000000000] & State_7_8=0.000000000000000] & State_9_6=0.000000000000000]] & State_2_2=0.000000000000000] & State_0_3=0.000000000000000]] & State_8_7=0.000000000000000] & State_1_2=0.000000000000000] & State_8_4=0.000000000000000]]]]]]]] & State_7_6=0.000000000000000]] & State_4_6=0.000000000000000]]]]] | [[true & 1.000000000000000>State_6_0] & [[[[[[[State_2_4=0.000000000000000 & [[[State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [[[[[[[State_2_2=0.000000000000000 & [[[[State_6_1=0.000000000000000 & [[[[State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [[[[State_3_1=0.000000000000000 & [[[State_9_0=0.000000000000000 & [[[[State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [[[[State_3_3=0.000000000000000 & [[[[[[[State_9_9=0.000000000000000 & [[[[State_6_5=0.000000000000000 & [[[[State_1_3=0.000000000000000 & [[[[State_1_1=0.000000000000000 & [[[[State_7_9=0.000000000000000 & [[[[State_9_5=0.000000000000000 & [[[[[State_8_0=0.000000000000000 & [[[[[[[State_9_8=0.000000000000000 & [[[[[[[[State_5_8=0.000000000000000 & [[[[[[[[State_8_6=0.000000000000000 & [true & State_3_8=0.000000000000000]] & State_2_3=0.000000000000000] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000] & State_7_3=0.000000000000000] & State_7_2=0.000000000000000]] & State_0_9=0.000000000000000] & State_1_8=0.000000000000000] & State_4_7=0.000000000000000] & State_2_8=0.000000000000000] & State_6_6=0.000000000000000] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000]] & State_0_1=0.000000000000000] & State_3_7=0.000000000000000] & State_1_7=0.000000000000000] & State_2_6=0.000000000000000] & State_5_3=0.000000000000000] & State_6_4=0.000000000000000]] & State_5_4=0.000000000000000] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000]] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000] & State_5_5=0.000000000000000]] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000] & State_9_1=0.000000000000000]] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000] & State_3_9=0.000000000000000]] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000]] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000] & State_8_5=0.000000000000000]] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000] & State_7_7=0.000000000000000] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000]] & State_6_7=0.000000000000000] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000]]] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000] & State_4_0=0.000000000000000]] & State_0_5=0.000000000000000] & State_9_4=0.000000000000000]] & State_8_3=0.000000000000000] & State_2_7=0.000000000000000] & State_7_4=0.000000000000000]]] & State_1_9=0.000000000000000] & State_0_4=0.000000000000000] & State_6_9=0.000000000000000]] & State_7_8=0.000000000000000] & State_9_6=0.000000000000000] & State_6_2=0.000000000000000]] & State_0_3=0.000000000000000] & State_0_2=0.000000000000000] & State_8_7=0.000000000000000] & State_1_2=0.000000000000000] & State_8_4=0.000000000000000] & State_4_9=0.000000000000000]]] & State_0_7=0.000000000000000] & State_0_8=0.000000000000000]] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000] & State_4_6=0.000000000000000] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000]]]]
normalized: EG [[[[[[State_4_6=0.000000000000000 & [[State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_5_0=0.000000000000000]] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000] & [true & 1.000000000000000>State_6_0]] | [[[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [1.000000000000000>State_8_1 & true]] & [false | [1.000000000000000>State_8_1 | false]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1052_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[true & 1.000000000000000>State_6_0] & [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [[[State_7_1=0.000000000000000 & [[[State_0_7=0.000000000000000 & [[State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [[State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [[[State_6_1=0.000000000000000 & [[[State_1_9=0.000000000000000 & [[State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [[State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [[[State_5_7=0.000000000000000 & [[[State_9_3=0.000000000000000 & [[State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [[State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [[[State_6_5=0.000000000000000 & [[[State_2_1=0.000000000000000 & [[State_3_9=0.000000000000000 & [State_1_6=0.000000000000000 & [[State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [[[State_9_5=0.000000000000000 & [[[[State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [[State_5_3=0.000000000000000 & [[State_1_7=0.000000000000000 & [[State_0_1=0.000000000000000 & [[[[[[State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [[State_3_2=0.000000000000000 & [[State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]] & State_6_8=0.000000000000000]] & State_3_5=0.000000000000000]]]]]]] & State_2_8=0.000000000000000] & State_6_6=0.000000000000000] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000]] & State_3_7=0.000000000000000]] & State_2_6=0.000000000000000]] & State_6_4=0.000000000000000]]] & State_3_4=0.000000000000000] & State_4_3=0.000000000000000] & State_2_0=0.000000000000000]] & State_5_2=0.000000000000000] & State_5_6=0.000000000000000]]]]]]] & State_7_0=0.000000000000000]]] & State_1_3=0.000000000000000]] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000]] & State_9_7=0.000000000000000] & State_1_0=0.000000000000000]]]]]]] & State_7_5=0.000000000000000]]] & State_6_7=0.000000000000000]] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000]] & State_8_2=0.000000000000000] & State_3_0=0.000000000000000]]]]]]] & State_2_7=0.000000000000000]]] & State_4_2=0.000000000000000]] & State_0_4=0.000000000000000] & State_6_9=0.000000000000000]] & State_7_8=0.000000000000000] & State_9_6=0.000000000000000]]]]]]] & State_8_4=0.000000000000000]]] & State_4_4=0.000000000000000]] & State_0_8=0.000000000000000] & State_2_4=0.000000000000000]] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000]]]]] & [[[false | 1.000000000000000>State_8_1] | false] & [[[State_2_9=0.000000000000000 & [[State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [[[State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [[State_4_9=0.000000000000000 & [[State_1_2=0.000000000000000 & [[State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [[[[[[State_8_3=0.000000000000000 & [[[[State_9_0=0.000000000000000 & [[State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [[State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [[[State_7_7=0.000000000000000 & [[[State_9_9=0.000000000000000 & [[State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [[State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [[[State_1_1=0.000000000000000 & [[[State_7_9=0.000000000000000 & [[State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [[State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [[[State_1_7=0.000000000000000 & [[[State_9_8=0.000000000000000 & [[State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [[State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [[[State_6_8=0.000000000000000 & [[[State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]] & State_2_3=0.000000000000000] & State_0_6=0.000000000000000]] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000]]]]]]] & State_2_8=0.000000000000000]]] & State_5_9=0.000000000000000]] & State_0_1=0.000000000000000] & State_3_7=0.000000000000000]] & State_2_6=0.000000000000000] & State_5_3=0.000000000000000]]]]]]] & State_9_5=0.000000000000000]]] & State_5_5=0.000000000000000]] & State_9_2=0.000000000000000] & State_9_1=0.000000000000000]] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000]]]]]]] & State_6_5=0.000000000000000]]] & State_8_5=0.000000000000000]] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000]] & State_1_4=0.000000000000000] & State_7_5=0.000000000000000]]]]]]] & State_5_7=0.000000000000000]]] & State_4_0=0.000000000000000]] & State_0_5=0.000000000000000] & State_9_4=0.000000000000000] & State_3_1=0.000000000000000]] & State_2_7=0.000000000000000] & State_7_4=0.000000000000000] & State_3_6=0.000000000000000] & State_4_2=0.000000000000000] & State_1_9=0.000000000000000]]]]]]]]]] & State_8_7=0.000000000000000]] & State_8_4=0.000000000000000]] & State_4_1=0.000000000000000]]]] & State_2_4=0.000000000000000] & State_7_1=0.000000000000000]]] & State_4_6=0.000000000000000]] & State_8_9=0.000000000000000] & [true & 1.000000000000000>State_8_1]]]]]
normalized: ~ [E [true U ~ [[[[[1.000000000000000>State_8_1 & true] & [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [false | [1.000000000000000>State_8_1 | false]]] & [[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=0.000000000000000 & [State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [State_0_8=0.000000000000000 & [State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [State_8_4=0.000000000000000 & [State_1_2=0.000000000000000 & [State_8_7=0.000000000000000 & [State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [State_2_2=0.000000000000000 & [State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [State_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [State_4_2=0.000000000000000 & [State_3_6=0.000000000000000 & [State_7_4=0.000000000000000 & [State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [State_4_0=0.000000000000000 & [State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [State_2_5=0.000000000000000 & [State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [State_3_3=0.000000000000000 & [State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [State_1_4=0.000000000000000 & [State_7_7=0.000000000000000 & [State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [State_9_7=0.000000000000000 & [State_6_5=0.000000000000000 & [State_1_5=0.000000000000000 & [State_8_8=0.000000000000000 & [State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_1_6=0.000000000000000 & [State_7_0=0.000000000000000 & [State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=0.000000000000000 & [State_9_2=0.000000000000000 & [State_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [State_3_4=0.000000000000000 & [State_5_4=0.000000000000000 & [State_8_0=0.000000000000000 & [State_6_4=0.000000000000000 & [State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [State_1_7=0.000000000000000 & [State_3_7=0.000000000000000 & [State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [State_5_9=0.000000000000000 & [State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [State_3_2=0.000000000000000 & [State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [State_2_3=0.000000000000000 & [State_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [1.000000000000000>State_6_0 & true]]]]]]

-> the formula is FALSE

FORMULA p_1053_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m11sec

STOP 1369909247

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

210 242 322 287 332 422 400 356 352 432 533 544 522 489 467 433 429 475 554 677 688 677 655 633 622 600 578 545 521 517 1032 1933 2743 2928 3016 3104 3181 3214 3335 3379 3434 3445 3588 3643 3687 3720 3753 3764 3799 3878 3934 4001 4079 4079 4068 4057 4046 4035 4013 4002 3980 3958 3947 3925 3892 3870 3856 3852 3951 4039 4116 4182 4237 4281 4314 4347 4347 4466 4584 4700 4814 4926 5036 5144 5250 5354 5456 5556 5566 5601 5651 5711 5781 5851 5921 6011 6111 6241 6451 6527
iterations count:100242 (90), effective:295 (0)

initing FirstDep: 0m0sec

6527
iterations count:1111 (1), effective:0 (0)
6527
iterations count:1111 (1), effective:0 (0)
6527
iterations count:1111 (1), effective:0 (0)
6527
iterations count:1111 (1), effective:0 (0)

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