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=ReachabilityMarkingComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1658
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/TokenRing-PT-010
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is TokenRing-PT-010, examination is ReachabilityMarkingComparison'
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 39: cluster1u41.lip6.fr (runId=136989898401294_n_39)
=====================================================================
runnning marcie on TokenRing-PT-010 (ReachabilityMarkingComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is TokenRing-PT-010, examination is ReachabilityMarkingComparison
=====================================================================

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

START 1369909311

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

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

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 121 NrTr: 1111)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m3sec


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



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

checking: AG [[[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_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_7_7 & 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_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_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_7_7 & 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_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_7_7 & 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_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 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=State_7_7] & 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_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]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_7_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m2sec

checking: AG [[[State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [[[State_7_6=0.000000000000000 & [State_7_1=0.000000000000000 & [[[[State_4_4=0.000000000000000 & [State_4_1=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_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_3_1=0.000000000000000 & [State_9_4=0.000000000000000 & [[[[[[[[[State_9_3=0.000000000000000 & [State_6_7=0.000000000000000 & [[State_4_8=0.000000000000000 & [State_7_5=0.000000000000000 & [[State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [[State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [[State_6_5=0.000000000000000 & [[[State_2_1=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_7_7 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_7_0=0.000000000000000] & State_1_6=0.000000000000000]] & State_3_9=0.000000000000000] & State_1_3=0.000000000000000]] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000]] & State_9_7=0.000000000000000]]] & State_9_9=0.000000000000000]]] & State_1_4=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_0_5=0.000000000000000]]] & State_8_3=0.000000000000000]]] & State_3_6=0.000000000000000]]]]]] & State_7_8=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_2_4=0.000000000000000]]] & State_5_0=0.000000000000000] & State_4_6=0.000000000000000]]] | [State_8_9=0.000000000000000 & [State_2_9=0.000000000000000 & [[State_5_0=0.000000000000000 & [[[[[State_0_7=0.000000000000000 & [[[[[[[State_0_2=0.000000000000000 & [[[[State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [[[[[[[[State_8_3=0.000000000000000 & [State_3_1=0.000000000000000 & [[State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [[State_3_0=0.000000000000000 & [[[[[[[[[[[State_5_1=0.000000000000000 & [[[[[[[[[[State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [State_6_0=0.000000000000000 & [State_1_6=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_1_7=0.000000000000000 & [[State_0_1=0.000000000000000 & [State_9_8=0.000000000000000 & [[[State_6_6=0.000000000000000 & [[State_4_7=0.000000000000000 & [State_1_8=0.000000000000000 & [State_0_9=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_7_7]]]]]]]]] & State_7_2=0.000000000000000] & State_5_8=0.000000000000000]]]] & State_2_8=0.000000000000000]] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000]]] & State_3_7=0.000000000000000]] & State_2_6=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_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_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_4_0=0.000000000000000]]] & State_9_4=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_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_4_4=0.000000000000000]] & State_0_8=0.000000000000000] & State_2_4=0.000000000000000] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000]] & State_4_6=0.000000000000000]]]]]
normalized: ~ [E [true U ~ [[[[State_2_9=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[State_0_4=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[State_7_5=0.000000000000000 & [State_1_4=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_8_6=0.000000000000000 & [State_3_8=0.000000000000000 & [true & 1.000000000000000=State_7_7]]] & State_2_3=0.000000000000000] & State_0_6=0.000000000000000] & State_6_8=0.000000000000000] & State_3_2=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_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_8_9=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 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=State_7_7] & 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_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_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_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]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_8_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[[State_4_6=0.000000000000000 & [[[State_7_1=0.000000000000000 & [State_2_4=0.000000000000000 & [[State_0_7=0.000000000000000 & [[State_4_1=0.000000000000000 & [[[[State_8_7=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_8_3=0.000000000000000 & [[[[[[[State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_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_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_5=0.000000000000000 & [[State_9_7=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_7_9=0.000000000000000 & [State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [State_5_2=0.000000000000000 & [[State_2_0=0.000000000000000 & [[State_3_4=0.000000000000000 & [[State_8_0=0.000000000000000 & [[State_5_3=0.000000000000000 & [State_2_6=0.000000000000000 & [[State_3_7=0.000000000000000 & [[[[State_4_5=0.000000000000000 & [[[[State_1_8=0.000000000000000 & [[[[[[State_3_2=0.000000000000000 & [[State_0_6=0.000000000000000 & [[State_8_6=0.000000000000000 & [[true & 1.000000000000000=State_7_7] & State_3_8=0.000000000000000]] & State_2_3=0.000000000000000]] & State_6_8=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_5_9=0.000000000000000] & State_9_8=0.000000000000000] & State_0_1=0.000000000000000]] & State_1_7=0.000000000000000]]] & State_6_4=0.000000000000000]] & State_5_4=0.000000000000000]] & State_4_3=0.000000000000000]] & State_9_5=0.000000000000000]]]]] & State_9_2=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_1_0=0.000000000000000]]]]]]]]]] & State_9_3=0.000000000000000] & State_2_5=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_2_7=0.000000000000000]]]]]]]]]]]]] & State_0_2=0.000000000000000]] & State_1_2=0.000000000000000] & State_8_4=0.000000000000000] & State_4_9=0.000000000000000]] & State_4_4=0.000000000000000]] & State_0_8=0.000000000000000]]] & State_7_6=0.000000000000000] & State_5_0=0.000000000000000]] & State_2_9=0.000000000000000] & State_8_9=0.000000000000000] & ~ [[[[[State_5_0=0.000000000000000 & [[State_7_1=0.000000000000000 & [[State_0_8=0.000000000000000 & [[State_4_4=0.000000000000000 & [[State_4_9=0.000000000000000 & [[State_1_2=0.000000000000000 & [[State_0_2=0.000000000000000 & [[[[State_9_6=0.000000000000000 & [State_7_8=0.000000000000000 & [State_6_1=0.000000000000000 & [[[State_1_9=0.000000000000000 & [[[State_7_4=0.000000000000000 & [[[[State_9_4=0.000000000000000 & [State_0_5=0.000000000000000 & [State_9_0=0.000000000000000 & [[[State_8_2=0.000000000000000 & [State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [[[State_6_7=0.000000000000000 & [[[[[State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [[[[[State_6_5=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_5_6=0.000000000000000 & [[State_9_5=0.000000000000000 & [State_2_0=0.000000000000000 & [State_4_3=0.000000000000000 & [[[[[[[State_1_7=0.000000000000000 & [[[[[State_4_5=0.000000000000000 & [State_6_6=0.000000000000000 & [[State_4_7=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 & [[[[[[true & 1.000000000000000=State_7_7] & 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_1_8=0.000000000000000]] & State_2_8=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_3_4=0.000000000000000]]]] & State_5_2=0.000000000000000]] & State_5_5=0.000000000000000] & State_7_9=0.000000000000000]]]]]]] & State_6_0=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_1_4=0.000000000000000] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=0.000000000000000]] & State_9_3=0.000000000000000] & State_2_5=0.000000000000000]]]] & State_3_0=0.000000000000000] & State_4_0=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_0_4=0.000000000000000] & State_6_9=0.000000000000000]]]] & State_6_2=0.000000000000000] & State_2_2=0.000000000000000] & State_0_3=0.000000000000000]] & State_8_7=0.000000000000000]] & State_8_4=0.000000000000000]] & State_4_1=0.000000000000000]] & State_0_7=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_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_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_0_9=0.000000000000000 & [State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [State_7_3=0.000000000000000 & [State_3_5=0.000000000000000 & [[[[[[[true & 1.000000000000000=State_7_7] & 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_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_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]] & [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_8_3=0.000000000000000 & [[[[[[State_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [[[[[[[[[[State_5_1=0.000000000000000 & [State_0_0=0.000000000000000 & [State_9_9=0.000000000000000 & [State_8_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_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 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=State_7_7] & 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_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_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_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_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_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_6_2=0.000000000000000] & State_2_2=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_9_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[State_8_9=0.000000000000000 & [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_2_2=0.000000000000000 & [[[[[[[State_1_9=0.000000000000000 & [[[[State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [[[[[[State_3_0=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_5_1=0.000000000000000 & [[State_9_9=0.000000000000000 & [[State_1_0=0.000000000000000 & [[State_6_5=0.000000000000000 & [[State_8_8=0.000000000000000 & [[State_1_3=0.000000000000000 & [[[State_1_6=0.000000000000000 & [[State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [State_8_1=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_7_7 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_5_5=0.000000000000000] & State_7_9=0.000000000000000] & State_9_2=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_9_7=0.000000000000000]] & State_8_5=0.000000000000000]] & State_0_0=0.000000000000000]]]]]]]] & State_2_5=0.000000000000000] & State_6_3=0.000000000000000] & State_5_7=0.000000000000000] & State_8_2=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_7_4=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_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_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [[State_7_6=0.000000000000000 & [[[[[State_4_4=0.000000000000000 & [[State_4_9=0.000000000000000 & [[[[State_0_2=0.000000000000000 & [State_0_3=0.000000000000000 & [[State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [[[[[[[[State_7_4=0.000000000000000 & [[[[[[[[[[State_5_7=0.000000000000000 & [State_6_3=0.000000000000000 & [[[State_6_7=0.000000000000000 & [[[[State_1_4=0.000000000000000 & [[[[State_8_5=0.000000000000000 & [State_1_0=0.000000000000000 & [[[State_1_5=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_7_9=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_5_3=0.000000000000000 & [[[State_3_7=0.000000000000000 & [State_0_1=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_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [[[State_3_8=0.000000000000000 & [1.000000000000000=State_7_7 & true]] & State_8_6=0.000000000000000] & State_2_3=0.000000000000000]]] & State_3_2=0.000000000000000] & State_3_5=0.000000000000000]]]]]]]]] & State_4_5=0.000000000000000] & State_5_9=0.000000000000000] & State_9_8=0.000000000000000]]] & State_1_7=0.000000000000000] & State_2_6=0.000000000000000]] & State_6_4=0.000000000000000]]]]] & State_2_0=0.000000000000000]]] & State_5_6=0.000000000000000] & State_5_5=0.000000000000000]] & State_9_2=0.000000000000000]]]] & State_7_0=0.000000000000000]] & State_6_0=0.000000000000000]] & State_1_3=0.000000000000000] & State_2_1=0.000000000000000] & State_8_8=0.000000000000000]] & State_6_5=0.000000000000000] & State_9_7=0.000000000000000]]] & State_9_9=0.000000000000000] & State_0_0=0.000000000000000] & State_5_1=0.000000000000000]] & State_7_5=0.000000000000000] & State_4_8=0.000000000000000] & State_3_3=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_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_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_2_2=0.000000000000000]]] & State_8_7=0.000000000000000] & State_1_2=0.000000000000000] & State_8_4=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_5_0=0.000000000000000]]]]]]]
normalized: ~ [E [true U ~ [[~ [[[State_2_9=0.000000000000000 & [State_4_6=0.000000000000000 & [State_5_0=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_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_7_7 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & 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_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_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_8_9=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_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_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [[[[State_5_5=0.000000000000000 & [State_5_6=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=State_7_7] & 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_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_7_9=0.000000000000000] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000]]] & State_7_0=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is TRUE

FORMULA p_10_markingcomparison_eq_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[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_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_6_9=0.000000000000000 & [State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [[[[State_2_7=0.000000000000000 & [State_8_3=0.000000000000000 & [[[[State_9_0=0.000000000000000 & [[State_3_0=0.000000000000000 & [[State_5_7=0.000000000000000 & [[[State_9_3=0.000000000000000 & [[State_3_3=0.000000000000000 & [[[[[State_0_0=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_1=0.000000000000000 & [State_9_1=0.000000000000000 & [[State_9_2=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_5_3=0.000000000000000 & [[[[[[State_5_9=0.000000000000000 & [[State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [State_4_7=0.000000000000000 & [[[[State_7_2=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_7_7]]]]]]] & State_3_5=0.000000000000000] & State_7_3=0.000000000000000]] & State_5_8=0.000000000000000] & State_0_9=0.000000000000000] & State_1_8=0.000000000000000]]]] & State_4_5=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_6_4=0.000000000000000]]]]]] & State_9_5=0.000000000000000]]] & State_5_5=0.000000000000000]]] & State_8_1=0.000000000000000]]] & State_7_0=0.000000000000000] & State_1_6=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_5_1=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_6_3=0.000000000000000]] & State_8_2=0.000000000000000]] & State_4_0=0.000000000000000]] & State_0_5=0.000000000000000] & State_9_4=0.000000000000000] & State_3_1=0.000000000000000]]] & State_7_4=0.000000000000000] & State_3_6=0.000000000000000] & State_4_2=0.000000000000000]]]] & State_6_1=0.000000000000000]] & State_9_6=0.000000000000000]]]]]]]]] & State_4_1=0.000000000000000] & State_4_4=0.000000000000000] & State_0_7=0.000000000000000]]] & State_7_1=0.000000000000000] & State_7_6=0.000000000000000]]]]] | [State_8_9=0.000000000000000 & [[State_4_6=0.000000000000000 & [[[State_7_1=0.000000000000000 & [[[State_0_7=0.000000000000000 & [State_4_4=0.000000000000000 & [State_4_1=0.000000000000000 & [State_4_9=0.000000000000000 & [[State_1_2=0.000000000000000 & [[[State_0_3=0.000000000000000 & [[State_6_2=0.000000000000000 & [State_9_6=0.000000000000000 & [[State_6_1=0.000000000000000 & [[State_0_4=0.000000000000000 & [State_1_9=0.000000000000000 & [[State_3_6=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_3_0=0.000000000000000 & [State_8_2=0.000000000000000 & [[State_6_3=0.000000000000000 & [[[State_6_7=0.000000000000000 & [[[[[[State_0_0=0.000000000000000 & [[State_8_5=0.000000000000000 & [[State_9_7=0.000000000000000 & [[[[State_2_1=0.000000000000000 & [State_1_3=0.000000000000000 & [State_3_9=0.000000000000000 & [[State_1_6=0.000000000000000 & [[State_1_1=0.000000000000000 & [State_9_1=0.000000000000000 & [[[[State_5_5=0.000000000000000 & [[State_5_2=0.000000000000000 & [[[State_4_3=0.000000000000000 & [[[[[[[[[[State_9_8=0.000000000000000 & [[[State_6_6=0.000000000000000 & [State_2_8=0.000000000000000 & [[[[State_5_8=0.000000000000000 & [State_7_2=0.000000000000000 & [[[[State_6_8=0.000000000000000 & [State_0_6=0.000000000000000 & [[[[true & 1.000000000000000=State_7_7] & 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_3=0.000000000000000]]] & State_0_9=0.000000000000000] & State_1_8=0.000000000000000] & State_4_7=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_8_0=0.000000000000000] & State_5_4=0.000000000000000] & State_3_4=0.000000000000000]] & State_2_0=0.000000000000000] & State_9_5=0.000000000000000]] & State_5_6=0.000000000000000]] & State_7_9=0.000000000000000] & State_9_2=0.000000000000000] & State_8_1=0.000000000000000]]] & State_7_0=0.000000000000000]] & State_6_0=0.000000000000000]]]] & State_8_8=0.000000000000000] & State_1_5=0.000000000000000] & State_6_5=0.000000000000000]] & State_1_0=0.000000000000000]] & State_9_9=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_9_3=0.000000000000000] & State_2_5=0.000000000000000]] & State_5_7=0.000000000000000]]] & State_4_0=0.000000000000000] & State_9_0=0.000000000000000]]]]]] & State_7_4=0.000000000000000]] & State_4_2=0.000000000000000]]] & State_6_9=0.000000000000000]] & State_7_8=0.000000000000000]]] & State_2_2=0.000000000000000]] & State_0_2=0.000000000000000] & State_8_7=0.000000000000000]] & State_8_4=0.000000000000000]]]]] & State_0_8=0.000000000000000] & State_2_4=0.000000000000000]] & State_7_6=0.000000000000000] & State_5_0=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_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_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_7_7 & 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_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_7_7 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_11_markingcomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[true & [true & 1.000000000000000<=State_9_8]] & [[[State_4_6!=0.000000000000000 & [[State_7_6!=0.000000000000000 & [[[[[[State_4_1!=0.000000000000000 & [[State_8_4!=0.000000000000000 & [State_1_2!=0.000000000000000 & [[State_0_2!=0.000000000000000 & [State_0_3!=0.000000000000000 & [[State_6_2!=0.000000000000000 & [State_9_6!=0.000000000000000 & [[State_6_1!=0.000000000000000 & [[State_0_4!=0.000000000000000 & [State_1_9!=0.000000000000000 & [[[[State_2_7!=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_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_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_2_8!=0.000000000000000 & [[[[[State_7_2!=0.000000000000000 & [[[State_3_2!=0.000000000000000 & [State_6_8!=0.000000000000000 & [[[[[1.000000000000000!=State_1_1 & true] & State_3_8!=0.000000000000000] & State_8_6!=0.000000000000000] & State_2_3!=0.000000000000000] & State_0_6!=0.000000000000000]]] & State_3_5!=0.000000000000000] & State_7_3!=0.000000000000000]] & State_5_8!=0.000000000000000] & State_0_9!=0.000000000000000] & State_1_8!=0.000000000000000] & State_4_7!=0.000000000000000]] & State_6_6!=0.000000000000000] & State_4_5!=0.000000000000000] & State_5_9!=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & State_9_4!=0.000000000000000]] & State_8_3!=0.000000000000000]] & State_7_4!=0.000000000000000] & State_3_6!=0.000000000000000] & State_4_2!=0.000000000000000]]] & State_6_9!=0.000000000000000]] & State_7_8!=0.000000000000000]]] & State_2_2!=0.000000000000000]]] & State_8_7!=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_1!=0.000000000000000]] & State_5_0!=0.000000000000000]] & State_2_9!=0.000000000000000] & State_8_9!=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[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_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_1_1 & true]]]]]]]]]]]]]]]]]]]]] & 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_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_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_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] & [[true & 1.000000000000000<=State_9_8] & true]]]]]

-> the formula is FALSE

FORMULA p_12_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[1.000000000000000<=State_9_8 & true] & true] | [[[State_4_6!=0.000000000000000 & [[[State_7_1!=0.000000000000000 & [[[[[[[[[[[[State_2_2!=0.000000000000000 & [[State_9_6!=0.000000000000000 & [State_7_8!=0.000000000000000 & [State_6_1!=0.000000000000000 & [[State_0_4!=0.000000000000000 & [[State_4_2!=0.000000000000000 & [State_3_6!=0.000000000000000 & [[State_2_7!=0.000000000000000 & [[State_3_1!=0.000000000000000 & [[State_0_5!=0.000000000000000 & [State_9_0!=0.000000000000000 & [State_4_0!=0.000000000000000 & [[State_8_2!=0.000000000000000 & [State_5_7!=0.000000000000000 & [State_6_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_5_1!=0.000000000000000 & [[[State_8_5!=0.000000000000000 & [State_1_0!=0.000000000000000 & [[State_6_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_7_0!=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_8_0!=0.000000000000000 & [[State_5_3!=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_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_3_5!=0.000000000000000 & [State_3_2!=0.000000000000000 & [[[[[[true & 1.000000000000000!=State_1_1] & 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_7_3!=0.000000000000000]]]]]]] & State_6_6!=0.000000000000000]]]]]]] & State_2_6!=0.000000000000000]] & State_6_4!=0.000000000000000]]]]]]]]]]] & State_9_2!=0.000000000000000] & State_8_1!=0.000000000000000]]] & State_1_6!=0.000000000000000]]]]]] & State_1_5!=0.000000000000000]] & State_9_7!=0.000000000000000]]] & State_9_9!=0.000000000000000] & State_0_0!=0.000000000000000]] & State_7_7!=0.000000000000000]]]]]] & State_9_3!=0.000000000000000] & State_2_5!=0.000000000000000]]]] & State_3_0!=0.000000000000000]]]] & State_9_4!=0.000000000000000]] & State_8_3!=0.000000000000000]] & State_7_4!=0.000000000000000]]] & State_1_9!=0.000000000000000]] & State_6_9!=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_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_6!=0.000000000000000] & State_5_0!=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 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000!=State_1_1] & 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_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_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_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]]]]]]]]]]]]]]]]]]]]] | [true & [1.000000000000000<=State_9_8 & true]]]]]]

-> the formula is FALSE

FORMULA p_13_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[true & 1.000000000000000<=State_9_8] & true] & [State_8_9!=0.000000000000000 & [State_2_9!=0.000000000000000 & [[[State_7_6!=0.000000000000000 & [[[[State_0_7!=0.000000000000000 & [[[[State_8_4!=0.000000000000000 & [[[[[State_2_2!=0.000000000000000 & [[[State_7_8!=0.000000000000000 & [[[[State_1_9!=0.000000000000000 & [[[[State_2_7!=0.000000000000000 & [[[[[State_9_0!=0.000000000000000 & [[[[State_5_7!=0.000000000000000 & [[[State_9_3!=0.000000000000000 & [[[[[[[[[State_9_9!=0.000000000000000 & [[[State_9_7!=0.000000000000000 & [[[[[[[[[State_7_0!=0.000000000000000 & [[[State_9_2!=0.000000000000000 & [State_7_9!=0.000000000000000 & [[[[[[[[State_5_4!=0.000000000000000 & [[[[[[[State_0_1!=0.000000000000000 & [State_9_8!=0.000000000000000 & [[[[[[[[[[[[[[[[[[true & 1.000000000000000!=State_1_1] & 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_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_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_8_1!=0.000000000000000] & State_9_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_1_5!=0.000000000000000] & State_6_5!=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_3_3!=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_4_0!=0.000000000000000]] & State_0_5!=0.000000000000000] & State_9_4!=0.000000000000000] & State_3_1!=0.000000000000000] & State_8_3!=0.000000000000000]] & State_7_4!=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_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_4_9!=0.000000000000000] & State_4_1!=0.000000000000000] & State_4_4!=0.000000000000000]] & State_0_8!=0.000000000000000] & State_2_4!=0.000000000000000] & State_7_1!=0.000000000000000]] & State_5_0!=0.000000000000000] & State_4_6!=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_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_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_1_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [true & [1.000000000000000<=State_9_8 & true]]]]]]

-> the formula is FALSE

FORMULA p_14_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m12sec

STOP 1369909324

--------------------
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)
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.1658: