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=Philosophers-PT-000050
export BK_EXAMINATION=CTLMarkingComparison
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/Philosophers-PT-000050
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is Philosophers-PT-000050, examination is CTLMarkingComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for Philosophers/000050 (P/T)

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

execution on node 1: quadhexa-2.u-paris10.fr (runId=136968525700257_n_1)
=====================================================================
runnning marcie on Philosophers-PT-000050 (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 Philosophers-PT-000050, examination is CTLMarkingComparison
=====================================================================

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

START 1369707574

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: 250 NrTr: 250)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m6sec


RS generation: 0m0sec


-> reachability set: #nodes 1280 (1.3e+03) #states 717,897,987,691,852,588,770,249 (23)



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

checking: AG [[[Think_48=0.000000000000000 & [Think_22=0.000000000000000 & [Think_50=0.000000000000000 & [Think_43=0.000000000000000 & [Think_28=0.000000000000000 & [Think_8=0.000000000000000 & [[[[[Think_14=0.000000000000000 & [Think_26=0.000000000000000 & [Think_42=0.000000000000000 & [Think_4=0.000000000000000 & [Think_31=0.000000000000000 & [Think_18=0.000000000000000 & [[[[[Think_32=0.000000000000000 & [Think_17=0.000000000000000 & [Think_24=0.000000000000000 & [Think_9=0.000000000000000 & [Think_23=0.000000000000000 & [Think_3=0.000000000000000 & [[[[[Think_21=0.000000000000000 & [Think_25=0.000000000000000 & [Think_35=0.000000000000000 & [Think_6=0.000000000000000 & [Think_34=0.000000000000000 & [Think_44=0.000000000000000 & [[[[Think_39=0.000000000000000 & [Think_1=0.000000000000000 & [[Think_13=0.000000000000000 & [[Think_7=0.000000000000000 & [[Think_27=0.000000000000000 & [[Think_40=0.000000000000000 & [1.000000000000000=Think_15 & true]] & Think_16=0.000000000000000]] & Think_36=0.000000000000000]] & Think_5=0.000000000000000]] & Think_11=0.000000000000000]]] & Think_12=0.000000000000000] & Think_38=0.000000000000000] & Think_41=0.000000000000000]]]]]]] & Think_49=0.000000000000000] & Think_33=0.000000000000000] & Think_45=0.000000000000000] & Think_19=0.000000000000000]]]]]]] & Think_20=0.000000000000000] & Think_47=0.000000000000000] & Think_30=0.000000000000000] & Think_29=0.000000000000000]]]]]]] & Think_46=0.000000000000000] & Think_10=0.000000000000000] & Think_37=0.000000000000000] & Think_2=0.000000000000000]]]]]]] & [[Catch2_3=0.000000000000000 & [[[Catch2_35=0.000000000000000 & [[[[[[[Catch2_17=0.000000000000000 & [[[Catch2_23=0.000000000000000 & [[[Catch2_20=0.000000000000000 & [[[[[[Catch2_48=0.000000000000000 & [[[[[[Catch2_21=0.000000000000000 & [[[Catch2_19=0.000000000000000 & [[[[[[Catch2_5=0.000000000000000 & [[[[[[Catch2_49=0.000000000000000 & [[[[[1.000000000000000=Catch2_1 & true] & Catch2_50=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_39=0.000000000000000]] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_33=0.000000000000000]] & Catch2_26=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_37=0.000000000000000]] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000]] & Catch2_2=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_24=0.000000000000000]] & Catch2_16=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_38=0.000000000000000]] & Catch2_22=0.000000000000000] & Catch2_29=0.000000000000000]] & Catch2_4=0.000000000000000] & Catch2_18=0.000000000000000]] & Catch2_28=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_7=0.000000000000000] & Catch2_31=0.000000000000000]] & Catch2_43=0.000000000000000] & Catch2_41=0.000000000000000]] & Catch2_10=0.000000000000000]]]
normalized: ~ [E [true U ~ [[[Think_48=0.000000000000000 & [Think_22=0.000000000000000 & [Think_50=0.000000000000000 & [Think_43=0.000000000000000 & [Think_28=0.000000000000000 & [Think_8=0.000000000000000 & [Think_2=0.000000000000000 & [Think_37=0.000000000000000 & [Think_10=0.000000000000000 & [Think_46=0.000000000000000 & [Think_14=0.000000000000000 & [Think_26=0.000000000000000 & [Think_42=0.000000000000000 & [Think_4=0.000000000000000 & [Think_31=0.000000000000000 & [Think_18=0.000000000000000 & [Think_29=0.000000000000000 & [Think_30=0.000000000000000 & [Think_47=0.000000000000000 & [Think_20=0.000000000000000 & [Think_32=0.000000000000000 & [Think_17=0.000000000000000 & [Think_24=0.000000000000000 & [Think_9=0.000000000000000 & [Think_23=0.000000000000000 & [[[[[[[[[[[[[[Think_12=0.000000000000000 & [Think_39=0.000000000000000 & [[Think_11=0.000000000000000 & [Think_13=0.000000000000000 & [[[[[[[true & 1.000000000000000=Think_15] & Think_40=0.000000000000000] & Think_16=0.000000000000000] & Think_27=0.000000000000000] & Think_36=0.000000000000000] & Think_7=0.000000000000000] & Think_5=0.000000000000000]]] & Think_1=0.000000000000000]]] & Think_38=0.000000000000000] & Think_41=0.000000000000000] & Think_44=0.000000000000000] & Think_34=0.000000000000000] & Think_6=0.000000000000000] & Think_35=0.000000000000000] & Think_25=0.000000000000000] & Think_21=0.000000000000000] & Think_49=0.000000000000000] & Think_33=0.000000000000000] & Think_45=0.000000000000000] & Think_19=0.000000000000000] & Think_3=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]] & [[[[Catch2_43=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[true & 1.000000000000000=Catch2_1] & Catch2_50=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_2=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_24=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_20=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_23=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_18=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_34=0.000000000000000] & Catch2_7=0.000000000000000] & Catch2_31=0.000000000000000] & Catch2_35=0.000000000000000]] & Catch2_41=0.000000000000000] & Catch2_3=0.000000000000000] & Catch2_10=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_1866_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[Think_48=0.000000000000000 & [[[[[[Think_2=0.000000000000000 & [Think_37=0.000000000000000 & [[[Think_14=0.000000000000000 & [[[Think_4=0.000000000000000 & [[[[[Think_47=0.000000000000000 & [[Think_32=0.000000000000000 & [Think_17=0.000000000000000 & [Think_24=0.000000000000000 & [Think_9=0.000000000000000 & [[Think_3=0.000000000000000 & [[[Think_33=0.000000000000000 & [Think_49=0.000000000000000 & [Think_21=0.000000000000000 & [[Think_35=0.000000000000000 & [[[[[[Think_12=0.000000000000000 & [[[[[Think_5=0.000000000000000 & [Think_7=0.000000000000000 & [Think_36=0.000000000000000 & [Think_27=0.000000000000000 & [Think_16=0.000000000000000 & [Think_40=0.000000000000000 & [true & 1.000000000000000=Think_15]]]]]]] & Think_13=0.000000000000000] & Think_11=0.000000000000000] & Think_1=0.000000000000000] & Think_39=0.000000000000000]] & Think_38=0.000000000000000] & Think_41=0.000000000000000] & Think_44=0.000000000000000] & Think_34=0.000000000000000] & Think_6=0.000000000000000]] & Think_25=0.000000000000000]]]] & Think_45=0.000000000000000] & Think_19=0.000000000000000]] & Think_23=0.000000000000000]]]]] & Think_20=0.000000000000000]] & Think_30=0.000000000000000] & Think_29=0.000000000000000] & Think_18=0.000000000000000] & Think_31=0.000000000000000]] & Think_42=0.000000000000000] & Think_26=0.000000000000000]] & Think_46=0.000000000000000] & Think_10=0.000000000000000]]] & Think_8=0.000000000000000] & Think_28=0.000000000000000] & Think_43=0.000000000000000] & Think_50=0.000000000000000] & Think_22=0.000000000000000]] | [[[[Catch2_43=0.000000000000000 & [[[Catch2_7=0.000000000000000 & [[[[[[[Catch2_4=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_38=0.000000000000000 & [[[[[Catch2_48=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_2=0.000000000000000 & [[[[[Catch2_37=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_5=0.000000000000000 & [[[[[Catch2_14=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_50=0.000000000000000 & [true & 1.000000000000000=Catch2_1]]]]]]] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_33=0.000000000000000]]]]]]] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000]]]]]]] & Catch2_16=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_15=0.000000000000000]]]]]]] & Catch2_18=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_34=0.000000000000000]] & Catch2_31=0.000000000000000] & Catch2_35=0.000000000000000]] & Catch2_41=0.000000000000000] & Catch2_3=0.000000000000000] & Catch2_10=0.000000000000000]]]
normalized: EG [[[Think_48=0.000000000000000 & [[[[[[Think_2=0.000000000000000 & [Think_37=0.000000000000000 & [Think_10=0.000000000000000 & [Think_46=0.000000000000000 & [Think_14=0.000000000000000 & [Think_26=0.000000000000000 & [Think_42=0.000000000000000 & [Think_4=0.000000000000000 & [Think_31=0.000000000000000 & [Think_18=0.000000000000000 & [Think_29=0.000000000000000 & [Think_30=0.000000000000000 & [Think_47=0.000000000000000 & [Think_20=0.000000000000000 & [Think_32=0.000000000000000 & [Think_17=0.000000000000000 & [Think_24=0.000000000000000 & [Think_9=0.000000000000000 & [Think_23=0.000000000000000 & [Think_3=0.000000000000000 & [Think_19=0.000000000000000 & [Think_45=0.000000000000000 & [Think_33=0.000000000000000 & [Think_49=0.000000000000000 & [Think_21=0.000000000000000 & [Think_25=0.000000000000000 & [Think_35=0.000000000000000 & [Think_6=0.000000000000000 & [Think_34=0.000000000000000 & [Think_44=0.000000000000000 & [Think_41=0.000000000000000 & [Think_38=0.000000000000000 & [Think_12=0.000000000000000 & [Think_39=0.000000000000000 & [Think_1=0.000000000000000 & [Think_11=0.000000000000000 & [Think_13=0.000000000000000 & [Think_5=0.000000000000000 & [Think_7=0.000000000000000 & [Think_36=0.000000000000000 & [Think_27=0.000000000000000 & [Think_16=0.000000000000000 & [Think_40=0.000000000000000 & [1.000000000000000=Think_15 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & Think_8=0.000000000000000] & Think_28=0.000000000000000] & Think_43=0.000000000000000] & Think_50=0.000000000000000] & Think_22=0.000000000000000]] | [Catch2_10=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_40=0.000000000000000 & [Catch2_46=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_50=0.000000000000000 & [1.000000000000000=Catch2_1 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1867_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[[[[Catch2_41=0.000000000000000 & [[[Catch2_31=0.000000000000000 & [Catch2_7=0.000000000000000 & [[[Catch2_42=0.000000000000000 & [Catch2_28=0.000000000000000 & [[[Catch2_4=0.000000000000000 & [[[Catch2_22=0.000000000000000 & [[[[Catch2_47=0.000000000000000 & [[[Catch2_48=0.000000000000000 & [Catch2_24=0.000000000000000 & [[[Catch2_32=0.000000000000000 & [[[[[[[[[Catch2_46=0.000000000000000 & [[[Catch2_33=0.000000000000000 & [[[[[[[[[[1.000000000000000=Catch2_1 & true] & Catch2_50=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000]] & Catch2_5=0.000000000000000] & Catch2_26=0.000000000000000]] & Catch2_40=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_2=0.000000000000000]] & Catch2_9=0.000000000000000] & Catch2_30=0.000000000000000]]] & Catch2_16=0.000000000000000] & Catch2_27=0.000000000000000]] & Catch2_15=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_20=0.000000000000000]] & Catch2_29=0.000000000000000] & Catch2_23=0.000000000000000]] & Catch2_18=0.000000000000000] & Catch2_17=0.000000000000000]]] & Catch2_8=0.000000000000000] & Catch2_34=0.000000000000000]]] & Catch2_35=0.000000000000000] & Catch2_43=0.000000000000000]] & Catch2_3=0.000000000000000] & Catch2_10=0.000000000000000] & [[[[[Think_28=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[Think_23=0.000000000000000 & [[[[[Think_49=0.000000000000000 & [[Think_25=0.000000000000000 & [[[[[[Think_38=0.000000000000000 & [[[[[[[[Think_36=0.000000000000000 & [[[Think_40=0.000000000000000 & [true & 1.000000000000000=Think_15]] & Think_16=0.000000000000000] & Think_27=0.000000000000000]] & Think_7=0.000000000000000] & Think_5=0.000000000000000] & Think_13=0.000000000000000] & Think_11=0.000000000000000] & Think_1=0.000000000000000] & Think_39=0.000000000000000] & Think_12=0.000000000000000]] & Think_41=0.000000000000000] & Think_44=0.000000000000000] & Think_34=0.000000000000000] & Think_6=0.000000000000000] & Think_35=0.000000000000000]] & Think_21=0.000000000000000]] & Think_33=0.000000000000000] & Think_45=0.000000000000000] & Think_19=0.000000000000000] & Think_3=0.000000000000000]] & Think_9=0.000000000000000] & Think_24=0.000000000000000] & Think_17=0.000000000000000] & Think_32=0.000000000000000] & Think_20=0.000000000000000] & Think_47=0.000000000000000] & Think_30=0.000000000000000] & Think_29=0.000000000000000] & Think_18=0.000000000000000] & Think_31=0.000000000000000] & Think_4=0.000000000000000] & Think_42=0.000000000000000] & Think_26=0.000000000000000] & Think_14=0.000000000000000] & Think_46=0.000000000000000] & Think_10=0.000000000000000] & Think_37=0.000000000000000] & Think_2=0.000000000000000] & Think_8=0.000000000000000]] & Think_43=0.000000000000000] & Think_50=0.000000000000000] & Think_22=0.000000000000000] & Think_48=0.000000000000000]]]
normalized: ~ [EG [~ [[[Think_48=0.000000000000000 & [Think_22=0.000000000000000 & [Think_50=0.000000000000000 & [Think_43=0.000000000000000 & [Think_28=0.000000000000000 & [Think_8=0.000000000000000 & [Think_2=0.000000000000000 & [Think_37=0.000000000000000 & [Think_10=0.000000000000000 & [Think_46=0.000000000000000 & [Think_14=0.000000000000000 & [Think_26=0.000000000000000 & [Think_42=0.000000000000000 & [Think_4=0.000000000000000 & [Think_31=0.000000000000000 & [Think_18=0.000000000000000 & [Think_29=0.000000000000000 & [Think_30=0.000000000000000 & [Think_47=0.000000000000000 & [Think_20=0.000000000000000 & [Think_32=0.000000000000000 & [Think_17=0.000000000000000 & [Think_24=0.000000000000000 & [Think_9=0.000000000000000 & [Think_23=0.000000000000000 & [Think_3=0.000000000000000 & [Think_19=0.000000000000000 & [Think_45=0.000000000000000 & [Think_33=0.000000000000000 & [Think_49=0.000000000000000 & [Think_21=0.000000000000000 & [Think_25=0.000000000000000 & [Think_35=0.000000000000000 & [[[[[[[[[[[Think_5=0.000000000000000 & [Think_7=0.000000000000000 & [Think_36=0.000000000000000 & [Think_27=0.000000000000000 & [Think_16=0.000000000000000 & [Think_40=0.000000000000000 & [1.000000000000000=Think_15 & true]]]]]]] & Think_13=0.000000000000000] & Think_11=0.000000000000000] & Think_1=0.000000000000000] & Think_39=0.000000000000000] & Think_12=0.000000000000000] & Think_38=0.000000000000000] & Think_41=0.000000000000000] & Think_44=0.000000000000000] & Think_34=0.000000000000000] & Think_6=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [Catch2_10=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_32=0.000000000000000 & [[[[[[[[[Catch2_46=0.000000000000000 & [Catch2_26=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_33=0.000000000000000 & [[[[[[[Catch2_36=0.000000000000000 & [[[true & 1.000000000000000=Catch2_1] & Catch2_50=0.000000000000000] & Catch2_6=0.000000000000000]] & Catch2_39=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000]]]]] & Catch2_40=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_2=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1868_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[[[Catch2_3=0.000000000000000 & [[[[[Catch2_7=0.000000000000000 & [[[[[[[Catch2_4=0.000000000000000 & [[[[[Catch2_38=0.000000000000000 & [[[Catch2_27=0.000000000000000 & [[[[[[[Catch2_2=0.000000000000000 & [[[[[Catch2_37=0.000000000000000 & [[[[[[[Catch2_13=0.000000000000000 & [[[[[Catch2_39=0.000000000000000 & [[[[true & 1.000000000000000=Catch2_1] & Catch2_50=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_36=0.000000000000000]] & Catch2_49=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000]] & Catch2_33=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_12=0.000000000000000]] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000]] & Catch2_32=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_24=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_16=0.000000000000000]] & Catch2_47=0.000000000000000] & Catch2_15=0.000000000000000]] & Catch2_20=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_23=0.000000000000000]] & Catch2_18=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_42=0.000000000000000] & Catch2_8=0.000000000000000] & Catch2_34=0.000000000000000]] & Catch2_31=0.000000000000000] & Catch2_35=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_41=0.000000000000000]] & Catch2_10=0.000000000000000] | [Think_48=0.000000000000000 & [[[[[[[[[[[[[Think_4=0.000000000000000 & [[[[Think_30=0.000000000000000 & [[[[[[[Think_23=0.000000000000000 & [[[[[[[[[[[[[Think_38=0.000000000000000 & [[Think_39=0.000000000000000 & [[[[[[[Think_27=0.000000000000000 & [[[true & 1.000000000000000=Think_15] & Think_40=0.000000000000000] & Think_16=0.000000000000000]] & Think_36=0.000000000000000] & Think_7=0.000000000000000] & Think_5=0.000000000000000] & Think_13=0.000000000000000] & Think_11=0.000000000000000] & Think_1=0.000000000000000]] & Think_12=0.000000000000000]] & Think_41=0.000000000000000] & Think_44=0.000000000000000] & Think_34=0.000000000000000] & Think_6=0.000000000000000] & Think_35=0.000000000000000] & Think_25=0.000000000000000] & Think_21=0.000000000000000] & Think_49=0.000000000000000] & Think_33=0.000000000000000] & Think_45=0.000000000000000] & Think_19=0.000000000000000] & Think_3=0.000000000000000]] & Think_9=0.000000000000000] & Think_24=0.000000000000000] & Think_17=0.000000000000000] & Think_32=0.000000000000000] & Think_20=0.000000000000000] & Think_47=0.000000000000000]] & Think_29=0.000000000000000] & Think_18=0.000000000000000] & Think_31=0.000000000000000]] & Think_42=0.000000000000000] & Think_26=0.000000000000000] & Think_14=0.000000000000000] & Think_46=0.000000000000000] & Think_10=0.000000000000000] & Think_37=0.000000000000000] & Think_2=0.000000000000000] & Think_8=0.000000000000000] & Think_28=0.000000000000000] & Think_43=0.000000000000000] & Think_50=0.000000000000000] & Think_22=0.000000000000000]]]]
normalized: E [true U [[Think_48=0.000000000000000 & [Think_22=0.000000000000000 & [Think_50=0.000000000000000 & [Think_43=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Think_41=0.000000000000000 & [Think_38=0.000000000000000 & [Think_12=0.000000000000000 & [Think_39=0.000000000000000 & [Think_1=0.000000000000000 & [Think_11=0.000000000000000 & [Think_13=0.000000000000000 & [Think_5=0.000000000000000 & [Think_7=0.000000000000000 & [Think_36=0.000000000000000 & [Think_27=0.000000000000000 & [Think_16=0.000000000000000 & [Think_40=0.000000000000000 & [1.000000000000000=Think_15 & true]]]]]]]]]]]]]] & Think_44=0.000000000000000] & Think_34=0.000000000000000] & Think_6=0.000000000000000] & Think_35=0.000000000000000] & Think_25=0.000000000000000] & Think_21=0.000000000000000] & Think_49=0.000000000000000] & Think_33=0.000000000000000] & Think_45=0.000000000000000] & Think_19=0.000000000000000] & Think_3=0.000000000000000] & Think_23=0.000000000000000] & Think_9=0.000000000000000] & Think_24=0.000000000000000] & Think_17=0.000000000000000] & Think_32=0.000000000000000] & Think_20=0.000000000000000] & Think_47=0.000000000000000] & Think_30=0.000000000000000] & Think_29=0.000000000000000] & Think_18=0.000000000000000] & Think_31=0.000000000000000] & Think_4=0.000000000000000] & Think_42=0.000000000000000] & Think_26=0.000000000000000] & Think_14=0.000000000000000] & Think_46=0.000000000000000] & Think_10=0.000000000000000] & Think_37=0.000000000000000] & Think_2=0.000000000000000] & Think_8=0.000000000000000] & Think_28=0.000000000000000]]]]] | [Catch2_10=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_48=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[Catch2_49=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_50=0.000000000000000 & [1.000000000000000=Catch2_1 & true]]]]]] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_46=0.000000000000000] & Catch2_40=0.000000000000000] & Catch2_12=0.000000000000000] & Catch2_37=0.000000000000000] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_2=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_24=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_1869_markingcomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [E [[[[[[[Catch2_31=0.000000000000000 & [[[Catch2_8=0.000000000000000 & [[[[[[[[[[[[[[[[[[[[[[[[[Catch2_37=0.000000000000000 & [[Catch2_40=0.000000000000000 & [[[[[[[[[[[[[[true & 1.000000000000000=Catch2_1] & Catch2_50=0.000000000000000] & Catch2_6=0.000000000000000] & Catch2_36=0.000000000000000] & Catch2_39=0.000000000000000] & Catch2_49=0.000000000000000] & Catch2_14=0.000000000000000] & Catch2_45=0.000000000000000] & Catch2_44=0.000000000000000] & Catch2_13=0.000000000000000] & Catch2_33=0.000000000000000] & Catch2_5=0.000000000000000] & Catch2_26=0.000000000000000] & Catch2_46=0.000000000000000]] & Catch2_12=0.000000000000000]] & Catch2_19=0.000000000000000] & Catch2_11=0.000000000000000] & Catch2_25=0.000000000000000] & Catch2_21=0.000000000000000] & Catch2_2=0.000000000000000] & Catch2_32=0.000000000000000] & Catch2_9=0.000000000000000] & Catch2_30=0.000000000000000] & Catch2_24=0.000000000000000] & Catch2_48=0.000000000000000] & Catch2_16=0.000000000000000] & Catch2_27=0.000000000000000] & Catch2_47=0.000000000000000] & Catch2_15=0.000000000000000] & Catch2_38=0.000000000000000] & Catch2_20=0.000000000000000] & Catch2_22=0.000000000000000] & Catch2_29=0.000000000000000] & Catch2_23=0.000000000000000] & Catch2_4=0.000000000000000] & Catch2_18=0.000000000000000] & Catch2_17=0.000000000000000] & Catch2_28=0.000000000000000] & Catch2_42=0.000000000000000]] & Catch2_34=0.000000000000000] & Catch2_7=0.000000000000000]] & Catch2_35=0.000000000000000] & Catch2_43=0.000000000000000] & Catch2_41=0.000000000000000] & Catch2_3=0.000000000000000] & Catch2_10=0.000000000000000] U AF [[[[[[[Think_8=0.000000000000000 & [[[Think_10=0.000000000000000 & [[[[[[[[Think_29=0.000000000000000 & [[[[[[[[[[[[[[[[[[[Think_44=0.000000000000000 & [[[[[[[[[[[[[Think_40=0.000000000000000 & [true & 1.000000000000000=Think_15]] & Think_16=0.000000000000000] & Think_27=0.000000000000000] & Think_36=0.000000000000000] & Think_7=0.000000000000000] & Think_5=0.000000000000000] & Think_13=0.000000000000000] & Think_11=0.000000000000000] & Think_1=0.000000000000000] & Think_39=0.000000000000000] & Think_12=0.000000000000000] & Think_38=0.000000000000000] & Think_41=0.000000000000000]] & Think_34=0.000000000000000] & Think_6=0.000000000000000] & Think_35=0.000000000000000] & Think_25=0.000000000000000] & Think_21=0.000000000000000] & Think_49=0.000000000000000] & Think_33=0.000000000000000] & Think_45=0.000000000000000] & Think_19=0.000000000000000] & Think_3=0.000000000000000] & Think_23=0.000000000000000] & Think_9=0.000000000000000] & Think_24=0.000000000000000] & Think_17=0.000000000000000] & Think_32=0.000000000000000] & Think_20=0.000000000000000] & Think_47=0.000000000000000] & Think_30=0.000000000000000]] & Think_18=0.000000000000000] & Think_31=0.000000000000000] & Think_4=0.000000000000000] & Think_42=0.000000000000000] & Think_26=0.000000000000000] & Think_14=0.000000000000000] & Think_46=0.000000000000000]] & Think_37=0.000000000000000] & Think_2=0.000000000000000]] & Think_28=0.000000000000000] & Think_43=0.000000000000000] & Think_50=0.000000000000000] & Think_22=0.000000000000000] & Think_48=0.000000000000000]]]]
normalized: E [true U E [[Catch2_10=0.000000000000000 & [Catch2_3=0.000000000000000 & [Catch2_41=0.000000000000000 & [Catch2_43=0.000000000000000 & [Catch2_35=0.000000000000000 & [Catch2_31=0.000000000000000 & [Catch2_7=0.000000000000000 & [Catch2_34=0.000000000000000 & [Catch2_8=0.000000000000000 & [Catch2_42=0.000000000000000 & [Catch2_28=0.000000000000000 & [Catch2_17=0.000000000000000 & [Catch2_18=0.000000000000000 & [Catch2_4=0.000000000000000 & [Catch2_23=0.000000000000000 & [Catch2_29=0.000000000000000 & [Catch2_22=0.000000000000000 & [Catch2_20=0.000000000000000 & [Catch2_38=0.000000000000000 & [Catch2_15=0.000000000000000 & [Catch2_47=0.000000000000000 & [Catch2_27=0.000000000000000 & [Catch2_16=0.000000000000000 & [Catch2_48=0.000000000000000 & [Catch2_24=0.000000000000000 & [Catch2_30=0.000000000000000 & [Catch2_9=0.000000000000000 & [Catch2_32=0.000000000000000 & [Catch2_2=0.000000000000000 & [Catch2_21=0.000000000000000 & [Catch2_25=0.000000000000000 & [Catch2_11=0.000000000000000 & [Catch2_19=0.000000000000000 & [Catch2_37=0.000000000000000 & [Catch2_12=0.000000000000000 & [Catch2_40=0.000000000000000 & [[Catch2_26=0.000000000000000 & [Catch2_5=0.000000000000000 & [Catch2_33=0.000000000000000 & [Catch2_13=0.000000000000000 & [Catch2_44=0.000000000000000 & [Catch2_45=0.000000000000000 & [Catch2_14=0.000000000000000 & [Catch2_49=0.000000000000000 & [Catch2_39=0.000000000000000 & [Catch2_36=0.000000000000000 & [Catch2_6=0.000000000000000 & [Catch2_50=0.000000000000000 & [1.000000000000000=Catch2_1 & true]]]]]]]]]]]]] & Catch2_46=0.000000000000000]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] U ~ [EG [~ [[Think_48=0.000000000000000 & [Think_22=0.000000000000000 & [Think_50=0.000000000000000 & [Think_43=0.000000000000000 & [Think_28=0.000000000000000 & [Think_8=0.000000000000000 & [Think_2=0.000000000000000 & [Think_37=0.000000000000000 & [Think_10=0.000000000000000 & [Think_46=0.000000000000000 & [Think_14=0.000000000000000 & [Think_26=0.000000000000000 & [Think_42=0.000000000000000 & [Think_4=0.000000000000000 & [Think_31=0.000000000000000 & [Think_18=0.000000000000000 & [Think_29=0.000000000000000 & [Think_30=0.000000000000000 & [Think_47=0.000000000000000 & [Think_20=0.000000000000000 & [Think_32=0.000000000000000 & [Think_17=0.000000000000000 & [Think_24=0.000000000000000 & [Think_9=0.000000000000000 & [Think_23=0.000000000000000 & [Think_3=0.000000000000000 & [Think_19=0.000000000000000 & [Think_45=0.000000000000000 & [Think_33=0.000000000000000 & [Think_49=0.000000000000000 & [Think_21=0.000000000000000 & [Think_25=0.000000000000000 & [Think_35=0.000000000000000 & [Think_6=0.000000000000000 & [Think_34=0.000000000000000 & [Think_44=0.000000000000000 & [Think_41=0.000000000000000 & [Think_38=0.000000000000000 & [Think_12=0.000000000000000 & [Think_39=0.000000000000000 & [Think_1=0.000000000000000 & [Think_11=0.000000000000000 & [Think_13=0.000000000000000 & [Think_5=0.000000000000000 & [Think_7=0.000000000000000 & [Think_36=0.000000000000000 & [Think_27=0.000000000000000 & [Think_16=0.000000000000000 & [Think_40=0.000000000000000 & [1.000000000000000=Think_15 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1870_markingcomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[true & [true & 1.000000000000000<=Think_50]] & [[[[[[[[[[[[[[[[[Eat_20=0.000000000000000 & [[[[[[[[Eat_9=0.000000000000000 & [[[[[[Eat_38=0.000000000000000 & [[[Eat_3=0.000000000000000 & [[[[[[[[[[[[[[Eat_4=0.000000000000000 & [[true & Eat_19=0.000000000000000] & Eat_37=0.000000000000000]] & Eat_35=0.000000000000000] & Eat_31=0.000000000000000] & Eat_13=0.000000000000000] & Eat_26=0.000000000000000] & Eat_46=0.000000000000000] & Eat_49=0.000000000000000] & Eat_47=0.000000000000000] & Eat_2=0.000000000000000] & Eat_11=0.000000000000000] & Eat_40=0.000000000000000] & Eat_7=0.000000000000000] & Eat_16=0.000000000000000] & Eat_33=0.000000000000000]] & Eat_27=0.000000000000000] & Eat_42=0.000000000000000]] & Eat_12=0.000000000000000] & Eat_18=0.000000000000000] & Eat_29=0.000000000000000] & Eat_8=0.000000000000000] & Eat_44=0.000000000000000]] & Eat_25=0.000000000000000] & Eat_15=0.000000000000000] & Eat_32=0.000000000000000] & Eat_22=0.000000000000000] & Eat_5=0.000000000000000] & Eat_10=0.000000000000000] & Eat_14=0.000000000000000]] & Eat_39=0.000000000000000] & Eat_6=0.000000000000000] & Eat_30=0.000000000000000] & Eat_43=0.000000000000000] & Eat_1=0.000000000000000] & Eat_45=0.000000000000000] & Eat_24=0.000000000000000] & Eat_23=0.000000000000000] & Eat_17=0.000000000000000] & Eat_21=0.000000000000000] & Eat_50=0.000000000000000] & Eat_36=0.000000000000000] & Eat_34=0.000000000000000] & Eat_48=0.000000000000000] & Eat_41=0.000000000000000] & [true & 1.000000000000000>Eat_28]]]]
normalized: ~ [E [true U ~ [[[[1.000000000000000>Eat_28 & true] & [Eat_41=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_40=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_19=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [[1.000000000000000<=Think_50 & true] & true]]]]]

-> the formula is FALSE

FORMULA p_1871_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[1.000000000000000<=Think_50 & true] & true] | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_38=0.000000000000000 & [[[[[[[[[Eat_2=0.000000000000000 & [[[[[[[[[[true & Eat_19=0.000000000000000] & Eat_37=0.000000000000000] & Eat_4=0.000000000000000] & Eat_35=0.000000000000000] & Eat_31=0.000000000000000] & Eat_13=0.000000000000000] & Eat_26=0.000000000000000] & Eat_46=0.000000000000000] & Eat_49=0.000000000000000] & Eat_47=0.000000000000000]] & Eat_11=0.000000000000000] & Eat_40=0.000000000000000] & Eat_7=0.000000000000000] & Eat_16=0.000000000000000] & Eat_33=0.000000000000000] & Eat_3=0.000000000000000] & Eat_27=0.000000000000000] & Eat_42=0.000000000000000]] & Eat_12=0.000000000000000] & Eat_18=0.000000000000000] & Eat_29=0.000000000000000] & Eat_8=0.000000000000000] & Eat_44=0.000000000000000] & Eat_9=0.000000000000000] & Eat_25=0.000000000000000] & Eat_15=0.000000000000000] & Eat_32=0.000000000000000] & Eat_22=0.000000000000000] & Eat_5=0.000000000000000] & Eat_10=0.000000000000000] & Eat_14=0.000000000000000] & Eat_20=0.000000000000000] & Eat_39=0.000000000000000] & Eat_6=0.000000000000000] & Eat_30=0.000000000000000] & Eat_43=0.000000000000000] & Eat_1=0.000000000000000] & Eat_45=0.000000000000000] & Eat_24=0.000000000000000] & Eat_23=0.000000000000000] & Eat_17=0.000000000000000] & Eat_21=0.000000000000000] & Eat_50=0.000000000000000] & Eat_36=0.000000000000000] & Eat_34=0.000000000000000] & Eat_48=0.000000000000000] & Eat_41=0.000000000000000] & [true & 1.000000000000000>Eat_28]]]]
normalized: ~ [E [true U ~ [[[[1.000000000000000>Eat_28 & true] & [Eat_41=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_40=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_19=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | [true & [1.000000000000000<=Think_50 & true]]]]]]

-> the formula is FALSE

FORMULA p_1872_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[[[true & 1.000000000000000>Eat_28] & [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[Eat_40=0.000000000000000 & [[[[[[[[[[[Eat_37=0.000000000000000 & [true & Eat_19=0.000000000000000]] & Eat_4=0.000000000000000] & Eat_35=0.000000000000000] & Eat_31=0.000000000000000] & Eat_13=0.000000000000000] & Eat_26=0.000000000000000] & Eat_46=0.000000000000000] & Eat_49=0.000000000000000] & Eat_47=0.000000000000000] & Eat_2=0.000000000000000] & Eat_11=0.000000000000000]] & Eat_7=0.000000000000000] & Eat_16=0.000000000000000] & Eat_33=0.000000000000000] & Eat_3=0.000000000000000] & Eat_27=0.000000000000000] & Eat_42=0.000000000000000] & Eat_38=0.000000000000000] & Eat_12=0.000000000000000] & Eat_18=0.000000000000000] & Eat_29=0.000000000000000] & Eat_8=0.000000000000000] & Eat_44=0.000000000000000] & Eat_9=0.000000000000000] & Eat_25=0.000000000000000] & Eat_15=0.000000000000000] & Eat_32=0.000000000000000] & Eat_22=0.000000000000000] & Eat_5=0.000000000000000] & Eat_10=0.000000000000000] & Eat_14=0.000000000000000] & Eat_20=0.000000000000000] & Eat_39=0.000000000000000] & Eat_6=0.000000000000000] & Eat_30=0.000000000000000] & Eat_43=0.000000000000000] & Eat_1=0.000000000000000] & Eat_45=0.000000000000000] & Eat_24=0.000000000000000] & Eat_23=0.000000000000000] & Eat_17=0.000000000000000] & Eat_21=0.000000000000000] & Eat_50=0.000000000000000] & Eat_36=0.000000000000000] & Eat_34=0.000000000000000] & Eat_48=0.000000000000000] & Eat_41=0.000000000000000]] & [true & [true & 1.000000000000000<=Think_50]]]]
normalized: EG [[[[1.000000000000000<=Think_50 & true] & true] & [[Eat_41=0.000000000000000 & [Eat_48=0.000000000000000 & [Eat_34=0.000000000000000 & [Eat_36=0.000000000000000 & [Eat_50=0.000000000000000 & [Eat_21=0.000000000000000 & [Eat_17=0.000000000000000 & [Eat_23=0.000000000000000 & [Eat_24=0.000000000000000 & [Eat_45=0.000000000000000 & [Eat_1=0.000000000000000 & [Eat_43=0.000000000000000 & [Eat_30=0.000000000000000 & [Eat_6=0.000000000000000 & [Eat_39=0.000000000000000 & [Eat_20=0.000000000000000 & [Eat_14=0.000000000000000 & [Eat_10=0.000000000000000 & [Eat_5=0.000000000000000 & [Eat_22=0.000000000000000 & [Eat_32=0.000000000000000 & [Eat_15=0.000000000000000 & [Eat_25=0.000000000000000 & [Eat_9=0.000000000000000 & [Eat_44=0.000000000000000 & [Eat_8=0.000000000000000 & [Eat_29=0.000000000000000 & [Eat_18=0.000000000000000 & [Eat_12=0.000000000000000 & [Eat_38=0.000000000000000 & [Eat_42=0.000000000000000 & [Eat_27=0.000000000000000 & [Eat_3=0.000000000000000 & [Eat_33=0.000000000000000 & [Eat_16=0.000000000000000 & [Eat_7=0.000000000000000 & [Eat_40=0.000000000000000 & [Eat_11=0.000000000000000 & [Eat_2=0.000000000000000 & [Eat_47=0.000000000000000 & [Eat_49=0.000000000000000 & [Eat_46=0.000000000000000 & [Eat_26=0.000000000000000 & [Eat_13=0.000000000000000 & [Eat_31=0.000000000000000 & [Eat_35=0.000000000000000 & [Eat_4=0.000000000000000 & [Eat_37=0.000000000000000 & [Eat_19=0.000000000000000 & true]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] & [1.000000000000000>Eat_28 & true]]]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1873_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m8sec

STOP 1369707582

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

1274
iterations count:1143 (4), effective:150 (0)

initing FirstDep: 0m0sec


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

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

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

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