Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

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

export BK_INPUT=Peterson-PT-3
export BK_EXAMINATION=ReachabilityFireability
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1656
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/Peterson-PT-3
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is Peterson-PT-3, examination is ReachabilityFireability'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

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

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

execution on node 37: cluster1u39.lip6.fr (runId=136966892301256_n_37)
=====================================================================
runnning marcie on Peterson-PT-3 (ReachabilityFireability)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is Peterson-PT-3, examination is ReachabilityFireability
=====================================================================

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

START 1369682526

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 244 NrTr: 332)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m49sec


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



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

checking: AG [[["BeginLoop_2_1_2" \in [1, oo) | ["BeginLoop_3_0_3" \in [1, oo) | ["BeginLoop_0_1_3" \in [1, oo) | ["BeginLoop_1_1_3" \in [1, oo) | ["BeginLoop_1_1_2" \in [1, oo) | [["BeginLoop_2_2_1" \in [1, oo) | [["BeginLoop_2_0_3" \in [1, oo) | ["BeginLoop_3_2_1" \in [1, oo) | ["BeginLoop_0_1_0" \in [1, oo) | [[["BeginLoop_3_2_3" \in [1, oo) | [["BeginLoop_2_1_1" \in [1, oo) | ["BeginLoop_3_1_2" \in [1, oo) | [["BeginLoop_1_0_2" \in [1, oo) | [[[[[["BeginLoop_3_0_2" \in [1, oo) | ["BeginLoop_1_0_0" \in [1, oo) | [[["BeginLoop_1_2_0" \in [1, oo) | [["BeginLoop_0_2_0" \in [1, oo) | [[["BeginLoop_3_2_0" \in [1, oo) | ["BeginLoop_0_1_1" \in [1, oo) | ["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | ["BeginLoop_0_2_3" \in [1, oo) | [[[[[[[[["BeginLoop_1_0_3" \in [1, oo) | "BeginLoop_0_0_3" \in [1, oo)] | "BeginLoop_2_1_0" \in [1, oo)] | "BeginLoop_1_2_1" \in [1, oo)] | "BeginLoop_2_2_3" \in [1, oo)] | "BeginLoop_1_2_3" \in [1, oo)] | "BeginLoop_3_0_1" \in [1, oo)] | "BeginLoop_2_2_0" \in [1, oo)] | "BeginLoop_3_1_0" \in [1, oo)] | "BeginLoop_2_0_0" \in [1, oo)]]]]]] | "BeginLoop_0_0_0" \in [1, oo)] | "BeginLoop_1_0_1" \in [1, oo)]] | "BeginLoop_2_1_3" \in [1, oo)]] | "BeginLoop_3_2_2" \in [1, oo)] | "BeginLoop_1_2_2" \in [1, oo)]]] | "BeginLoop_0_1_2" \in [1, oo)] | "BeginLoop_0_0_2" \in [1, oo)] | "BeginLoop_0_2_2" \in [1, oo)] | "BeginLoop_0_2_1" \in [1, oo)] | "BeginLoop_3_1_3" \in [1, oo)]] | "BeginLoop_3_1_1" \in [1, oo)]]] | "BeginLoop_0_0_1" \in [1, oo)]] | "BeginLoop_2_2_2" \in [1, oo)] | "BeginLoop_3_0_0" \in [1, oo)]]]] | "BeginLoop_1_1_0" \in [1, oo)]] | "BeginLoop_1_1_1" \in [1, oo)]]]]]] & ["Turn_0_0" \in [1, oo) && "TestTurn_0_0" \in [1, oo) | [[[[[["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | [[["Turn_0_3" \in [1, oo) && "TestTurn_3_0" \in [1, oo) | ["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)]] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)]] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "TestTurn_2_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "TestTurn_3_2" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "TestTurn_2_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "TestTurn_1_0" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[["BeginLoop_2_1_2" \in [1, oo) | ["BeginLoop_3_0_3" \in [1, oo) | ["BeginLoop_0_1_3" \in [1, oo) | ["BeginLoop_1_1_3" \in [1, oo) | ["BeginLoop_1_1_2" \in [1, oo) | [["BeginLoop_2_2_1" \in [1, oo) | [["BeginLoop_2_0_3" \in [1, oo) | ["BeginLoop_3_2_1" \in [1, oo) | ["BeginLoop_0_1_0" \in [1, oo) | [[["BeginLoop_3_2_3" \in [1, oo) | [["BeginLoop_2_1_1" \in [1, oo) | ["BeginLoop_3_1_2" \in [1, oo) | [["BeginLoop_1_0_2" \in [1, oo) | [[[[[["BeginLoop_3_0_2" \in [1, oo) | ["BeginLoop_1_0_0" \in [1, oo) | [[["BeginLoop_1_2_0" \in [1, oo) | [["BeginLoop_0_2_0" \in [1, oo) | [[["BeginLoop_3_2_0" \in [1, oo) | ["BeginLoop_0_1_1" \in [1, oo) | ["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | ["BeginLoop_0_2_3" \in [1, oo) | [[[[[[[[["BeginLoop_1_0_3" \in [1, oo) | "BeginLoop_0_0_3" \in [1, oo)] | "BeginLoop_2_1_0" \in [1, oo)] | "BeginLoop_1_2_1" \in [1, oo)] | "BeginLoop_2_2_3" \in [1, oo)] | "BeginLoop_1_2_3" \in [1, oo)] | "BeginLoop_3_0_1" \in [1, oo)] | "BeginLoop_2_2_0" \in [1, oo)] | "BeginLoop_3_1_0" \in [1, oo)] | "BeginLoop_2_0_0" \in [1, oo)]]]]]] | "BeginLoop_0_0_0" \in [1, oo)] | "BeginLoop_1_0_1" \in [1, oo)]] | "BeginLoop_2_1_3" \in [1, oo)]] | "BeginLoop_3_2_2" \in [1, oo)] | "BeginLoop_1_2_2" \in [1, oo)]]] | "BeginLoop_0_1_2" \in [1, oo)] | "BeginLoop_0_0_2" \in [1, oo)] | "BeginLoop_0_2_2" \in [1, oo)] | "BeginLoop_0_2_1" \in [1, oo)] | "BeginLoop_3_1_3" \in [1, oo)]] | "BeginLoop_3_1_1" \in [1, oo)]]] | "BeginLoop_0_0_1" \in [1, oo)]] | "BeginLoop_2_2_2" \in [1, oo)] | "BeginLoop_3_0_0" \in [1, oo)]]]] | "BeginLoop_1_1_0" \in [1, oo)]] | "BeginLoop_1_1_1" \in [1, oo)]]]]]] & ["Turn_0_0" \in [1, oo) && "TestTurn_0_0" \in [1, oo) | [[[[[["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | [[["Turn_0_3" \in [1, oo) && "TestTurn_3_0" \in [1, oo) | ["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)]] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)]] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "TestTurn_2_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "TestTurn_3_2" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "TestTurn_2_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "TestTurn_1_0" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m13sec

checking: AG [[["Turn_0_0" \in [1, oo) && "TestTurn_0_0" \in [1, oo) | [[["Turn_2_3" \in [1, oo) && "TestTurn_3_2" \in [1, oo) | [[["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | [["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | [["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)]] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)]] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo)]] | "Turn_2_2" \in [1, oo) && "TestTurn_2_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "TestTurn_1_0" \in [1, oo)]] | ["BeginLoop_2_1_2" \in [1, oo) | [[[[[["BeginLoop_2_2_1" \in [1, oo) | ["BeginLoop_1_1_0" \in [1, oo) | ["BeginLoop_2_0_3" \in [1, oo) | [["BeginLoop_0_1_0" \in [1, oo) | [[[["BeginLoop_0_0_1" \in [1, oo) | ["BeginLoop_2_1_1" \in [1, oo) | [["BeginLoop_3_1_1" \in [1, oo) | ["BeginLoop_1_0_2" \in [1, oo) | [["BeginLoop_0_2_1" \in [1, oo) | [["BeginLoop_0_0_2" \in [1, oo) | ["BeginLoop_0_1_2" \in [1, oo) | ["BeginLoop_3_0_2" \in [1, oo) | ["BeginLoop_1_0_0" \in [1, oo) | [["BeginLoop_3_2_2" \in [1, oo) | [["BeginLoop_2_1_3" \in [1, oo) | ["BeginLoop_0_2_0" \in [1, oo) | [["BeginLoop_0_0_0" \in [1, oo) | ["BeginLoop_3_2_0" \in [1, oo) | ["BeginLoop_0_1_1" \in [1, oo) | ["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | ["BeginLoop_0_2_3" \in [1, oo) | ["BeginLoop_2_0_0" \in [1, oo) | ["BeginLoop_3_1_0" \in [1, oo) | ["BeginLoop_2_2_0" \in [1, oo) | ["BeginLoop_3_0_1" \in [1, oo) | ["BeginLoop_1_2_3" \in [1, oo) | ["BeginLoop_2_2_3" \in [1, oo) | ["BeginLoop_1_2_1" \in [1, oo) | ["BeginLoop_2_1_0" \in [1, oo) | ["BeginLoop_0_0_3" \in [1, oo) | "BeginLoop_1_0_3" \in [1, oo)]]]]]]]]]]]]]]] | "BeginLoop_1_0_1" \in [1, oo)]]] | "BeginLoop_1_2_0" \in [1, oo)]] | "BeginLoop_1_2_2" \in [1, oo)]]]]] | "BeginLoop_0_2_2" \in [1, oo)]] | "BeginLoop_3_1_3" \in [1, oo)]]] | "BeginLoop_3_1_2" \in [1, oo)]]] | "BeginLoop_3_2_3" \in [1, oo)] | "BeginLoop_2_2_2" \in [1, oo)] | "BeginLoop_3_0_0" \in [1, oo)]] | "BeginLoop_3_2_1" \in [1, oo)]]]] | "BeginLoop_1_1_1" \in [1, oo)] | "BeginLoop_1_1_2" \in [1, oo)] | "BeginLoop_1_1_3" \in [1, oo)] | "BeginLoop_0_1_3" \in [1, oo)] | "BeginLoop_3_0_3" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[[[[[["BeginLoop_1_1_2" \in [1, oo) | ["BeginLoop_1_1_1" \in [1, oo) | [["BeginLoop_1_1_0" \in [1, oo) | ["BeginLoop_2_0_3" \in [1, oo) | ["BeginLoop_3_2_1" \in [1, oo) | ["BeginLoop_0_1_0" \in [1, oo) | ["BeginLoop_3_0_0" \in [1, oo) | ["BeginLoop_2_2_2" \in [1, oo) | ["BeginLoop_3_2_3" \in [1, oo) | ["BeginLoop_0_0_1" \in [1, oo) | [["BeginLoop_3_1_2" \in [1, oo) | ["BeginLoop_3_1_1" \in [1, oo) | [["BeginLoop_3_1_3" \in [1, oo) | [["BeginLoop_0_2_2" \in [1, oo) | ["BeginLoop_0_0_2" \in [1, oo) | ["BeginLoop_0_1_2" \in [1, oo) | ["BeginLoop_3_0_2" \in [1, oo) | [["BeginLoop_1_2_2" \in [1, oo) | [["BeginLoop_1_2_0" \in [1, oo) | ["BeginLoop_2_1_3" \in [1, oo) | [["BeginLoop_1_0_1" \in [1, oo) | [[[["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | ["BeginLoop_0_2_3" \in [1, oo) | [["BeginLoop_3_1_0" \in [1, oo) | [["BeginLoop_3_0_1" \in [1, oo) | [["BeginLoop_2_2_3" \in [1, oo) | ["BeginLoop_1_2_1" \in [1, oo) | ["BeginLoop_2_1_0" \in [1, oo) | ["BeginLoop_0_0_3" \in [1, oo) | "BeginLoop_1_0_3" \in [1, oo)]]]] | "BeginLoop_1_2_3" \in [1, oo)]] | "BeginLoop_2_2_0" \in [1, oo)]] | "BeginLoop_2_0_0" \in [1, oo)]]]] | "BeginLoop_0_1_1" \in [1, oo)] | "BeginLoop_3_2_0" \in [1, oo)] | "BeginLoop_0_0_0" \in [1, oo)]] | "BeginLoop_0_2_0" \in [1, oo)]]] | "BeginLoop_3_2_2" \in [1, oo)]] | "BeginLoop_1_0_0" \in [1, oo)]]]]] | "BeginLoop_0_2_1" \in [1, oo)]] | "BeginLoop_1_0_2" \in [1, oo)]]] | "BeginLoop_2_1_1" \in [1, oo)]]]]]]]]] | "BeginLoop_2_2_1" \in [1, oo)]]] | "BeginLoop_1_1_3" \in [1, oo)] | "BeginLoop_0_1_3" \in [1, oo)] | "BeginLoop_3_0_3" \in [1, oo)] | "BeginLoop_2_1_2" \in [1, oo)] | ["Turn_0_0" \in [1, oo) && "TestTurn_0_0" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "TestTurn_1_0" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "TestTurn_2_2" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "TestTurn_3_2" \in [1, oo) | ["TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | ["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | [[[[["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_3_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m12sec

checking: AG [[[["TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo) | ["TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo) | [["Turn_0_2" \in [1, oo) && "TestTurn_2_0" \in [1, oo) | ["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "TestTurn_1_2" \in [1, oo) | [["TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo) | "TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)]] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)]]]]] | "Turn_2_3" \in [1, oo) && "TestTurn_3_2" \in [1, oo)]]] | "TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo)] & ["BeginLoop_2_1_2" \in [1, oo) | [[["BeginLoop_1_1_3" \in [1, oo) | ["BeginLoop_1_1_2" \in [1, oo) | ["BeginLoop_1_1_1" \in [1, oo) | ["BeginLoop_2_2_1" \in [1, oo) | [["BeginLoop_2_0_3" \in [1, oo) | ["BeginLoop_3_2_1" \in [1, oo) | ["BeginLoop_0_1_0" \in [1, oo) | ["BeginLoop_3_0_0" \in [1, oo) | ["BeginLoop_2_2_2" \in [1, oo) | ["BeginLoop_3_2_3" \in [1, oo) | [[[[["BeginLoop_1_0_2" \in [1, oo) | [["BeginLoop_0_2_1" \in [1, oo) | ["BeginLoop_0_2_2" \in [1, oo) | ["BeginLoop_0_0_2" \in [1, oo) | ["BeginLoop_0_1_2" \in [1, oo) | [[[["BeginLoop_3_2_2" \in [1, oo) | [[[[[[["BeginLoop_0_1_1" \in [1, oo) | ["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | ["BeginLoop_0_2_3" \in [1, oo) | ["BeginLoop_2_0_0" \in [1, oo) | ["BeginLoop_3_1_0" \in [1, oo) | [[["BeginLoop_1_2_3" \in [1, oo) | ["BeginLoop_2_2_3" \in [1, oo) | [["BeginLoop_2_1_0" \in [1, oo) | ["BeginLoop_1_0_3" \in [1, oo) | "BeginLoop_0_0_3" \in [1, oo)]] | "BeginLoop_1_2_1" \in [1, oo)]]] | "BeginLoop_3_0_1" \in [1, oo)] | "BeginLoop_2_2_0" \in [1, oo)]]]]]]] | "BeginLoop_3_2_0" \in [1, oo)] | "BeginLoop_0_0_0" \in [1, oo)] | "BeginLoop_1_0_1" \in [1, oo)] | "BeginLoop_0_2_0" \in [1, oo)] | "BeginLoop_2_1_3" \in [1, oo)] | "BeginLoop_1_2_0" \in [1, oo)]] | "BeginLoop_1_2_2" \in [1, oo)] | "BeginLoop_1_0_0" \in [1, oo)] | "BeginLoop_3_0_2" \in [1, oo)]]]]] | "BeginLoop_3_1_3" \in [1, oo)]] | "BeginLoop_3_1_1" \in [1, oo)] | "BeginLoop_3_1_2" \in [1, oo)] | "BeginLoop_2_1_1" \in [1, oo)] | "BeginLoop_0_0_1" \in [1, oo)]]]]]]] | "BeginLoop_1_1_0" \in [1, oo)]]]]] | "BeginLoop_0_1_3" \in [1, oo)] | "BeginLoop_3_0_3" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[[[[[[[[[[[[[[[[[["BeginLoop_3_1_2" \in [1, oo) | ["BeginLoop_3_1_1" \in [1, oo) | [["BeginLoop_3_1_3" \in [1, oo) | [[[[["BeginLoop_3_0_2" \in [1, oo) | ["BeginLoop_1_0_0" \in [1, oo) | ["BeginLoop_1_2_2" \in [1, oo) | [["BeginLoop_1_2_0" \in [1, oo) | ["BeginLoop_2_1_3" \in [1, oo) | ["BeginLoop_0_2_0" \in [1, oo) | ["BeginLoop_1_0_1" \in [1, oo) | ["BeginLoop_0_0_0" \in [1, oo) | ["BeginLoop_3_2_0" \in [1, oo) | [[[[[[["BeginLoop_2_2_0" \in [1, oo) | ["BeginLoop_3_0_1" \in [1, oo) | [[["BeginLoop_1_2_1" \in [1, oo) | [["BeginLoop_0_0_3" \in [1, oo) | "BeginLoop_1_0_3" \in [1, oo)] | "BeginLoop_2_1_0" \in [1, oo)]] | "BeginLoop_2_2_3" \in [1, oo)] | "BeginLoop_1_2_3" \in [1, oo)]]] | "BeginLoop_3_1_0" \in [1, oo)] | "BeginLoop_2_0_0" \in [1, oo)] | "BeginLoop_0_2_3" \in [1, oo)] | "BeginLoop_2_0_1" \in [1, oo)] | "BeginLoop_2_0_2" \in [1, oo)] | "BeginLoop_0_1_1" \in [1, oo)]]]]]]] | "BeginLoop_3_2_2" \in [1, oo)]]]] | "BeginLoop_0_1_2" \in [1, oo)] | "BeginLoop_0_0_2" \in [1, oo)] | "BeginLoop_0_2_2" \in [1, oo)] | "BeginLoop_0_2_1" \in [1, oo)]] | "BeginLoop_1_0_2" \in [1, oo)]]] | "BeginLoop_2_1_1" \in [1, oo)] | "BeginLoop_0_0_1" \in [1, oo)] | "BeginLoop_3_2_3" \in [1, oo)] | "BeginLoop_2_2_2" \in [1, oo)] | "BeginLoop_3_0_0" \in [1, oo)] | "BeginLoop_0_1_0" \in [1, oo)] | "BeginLoop_3_2_1" \in [1, oo)] | "BeginLoop_2_0_3" \in [1, oo)] | "BeginLoop_1_1_0" \in [1, oo)] | "BeginLoop_2_2_1" \in [1, oo)] | "BeginLoop_1_1_1" \in [1, oo)] | "BeginLoop_1_1_2" \in [1, oo)] | "BeginLoop_1_1_3" \in [1, oo)] | "BeginLoop_0_1_3" \in [1, oo)] | "BeginLoop_3_0_3" \in [1, oo)] | "BeginLoop_2_1_2" \in [1, oo)] & ["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | [[["Turn_2_3" \in [1, oo) && "TestTurn_3_2" \in [1, oo) | [[[[["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | [["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)]] | "Turn_2_1" \in [1, oo) && "TestTurn_1_2" \in [1, oo)] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "TestTurn_2_0" \in [1, oo)]] | "TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo)] | "TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: AG [[[[[[[[["BeginLoop_2_2_1" \in [1, oo) | ["BeginLoop_1_1_0" \in [1, oo) | ["BeginLoop_2_0_3" \in [1, oo) | ["BeginLoop_3_2_1" \in [1, oo) | [["BeginLoop_3_0_0" \in [1, oo) | [["BeginLoop_3_2_3" \in [1, oo) | ["BeginLoop_0_0_1" \in [1, oo) | ["BeginLoop_2_1_1" \in [1, oo) | [[[["BeginLoop_3_1_3" \in [1, oo) | ["BeginLoop_0_2_1" \in [1, oo) | ["BeginLoop_0_2_2" \in [1, oo) | [["BeginLoop_0_1_2" \in [1, oo) | ["BeginLoop_3_0_2" \in [1, oo) | [["BeginLoop_1_2_2" \in [1, oo) | ["BeginLoop_3_2_2" \in [1, oo) | ["BeginLoop_1_2_0" \in [1, oo) | [[["BeginLoop_1_0_1" \in [1, oo) | [[[["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | ["BeginLoop_0_2_3" \in [1, oo) | [[["BeginLoop_2_2_0" \in [1, oo) | [[["BeginLoop_2_2_3" \in [1, oo) | ["BeginLoop_1_2_1" \in [1, oo) | [["BeginLoop_1_0_3" \in [1, oo) | "BeginLoop_0_0_3" \in [1, oo)] | "BeginLoop_2_1_0" \in [1, oo)]]] | "BeginLoop_1_2_3" \in [1, oo)] | "BeginLoop_3_0_1" \in [1, oo)]] | "BeginLoop_3_1_0" \in [1, oo)] | "BeginLoop_2_0_0" \in [1, oo)]]]] | "BeginLoop_0_1_1" \in [1, oo)] | "BeginLoop_3_2_0" \in [1, oo)] | "BeginLoop_0_0_0" \in [1, oo)]] | "BeginLoop_0_2_0" \in [1, oo)] | "BeginLoop_2_1_3" \in [1, oo)]]]] | "BeginLoop_1_0_0" \in [1, oo)]]] | "BeginLoop_0_0_2" \in [1, oo)]]]] | "BeginLoop_1_0_2" \in [1, oo)] | "BeginLoop_3_1_1" \in [1, oo)] | "BeginLoop_3_1_2" \in [1, oo)]]]] | "BeginLoop_2_2_2" \in [1, oo)]] | "BeginLoop_0_1_0" \in [1, oo)]]]]] | "BeginLoop_1_1_1" \in [1, oo)] | "BeginLoop_1_1_2" \in [1, oo)] | "BeginLoop_1_1_3" \in [1, oo)] | "BeginLoop_0_1_3" \in [1, oo)] | "BeginLoop_3_0_3" \in [1, oo)] | "BeginLoop_2_1_2" \in [1, oo)] | ["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | [["TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo) | [[["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | [[["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["Turn_0_3" \in [1, oo) && "TestTurn_3_0" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "TestTurn_0_2" \in [1, oo) | "TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)]]] | "Turn_2_1" \in [1, oo) && "TestTurn_1_2" \in [1, oo)] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)]] | "TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo)] | "TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo)]] | "TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | ["TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo) | [["TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | ["TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | [["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "TestTurn_1_2" \in [1, oo) | [[["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "Turn_2_0" \in [1, oo) && "TestTurn_0_2" \in [1, oo)] | "Turn_0_3" \in [1, oo) && "TestTurn_3_0" \in [1, oo)] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)]]] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)]]] | "TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo)]]] | ["BeginLoop_2_1_2" \in [1, oo) | ["BeginLoop_3_0_3" \in [1, oo) | ["BeginLoop_0_1_3" \in [1, oo) | ["BeginLoop_1_1_3" \in [1, oo) | ["BeginLoop_1_1_2" \in [1, oo) | ["BeginLoop_1_1_1" \in [1, oo) | [[[[["BeginLoop_0_1_0" \in [1, oo) | [["BeginLoop_2_2_2" \in [1, oo) | [[[["BeginLoop_3_1_2" \in [1, oo) | ["BeginLoop_3_1_1" \in [1, oo) | ["BeginLoop_1_0_2" \in [1, oo) | [[[["BeginLoop_0_0_2" \in [1, oo) | [[["BeginLoop_1_0_0" \in [1, oo) | [[[["BeginLoop_2_1_3" \in [1, oo) | ["BeginLoop_0_2_0" \in [1, oo) | [["BeginLoop_0_0_0" \in [1, oo) | ["BeginLoop_3_2_0" \in [1, oo) | ["BeginLoop_0_1_1" \in [1, oo) | [[[["BeginLoop_2_0_0" \in [1, oo) | ["BeginLoop_3_1_0" \in [1, oo) | [["BeginLoop_3_0_1" \in [1, oo) | ["BeginLoop_1_2_3" \in [1, oo) | [[["BeginLoop_2_1_0" \in [1, oo) | ["BeginLoop_0_0_3" \in [1, oo) | "BeginLoop_1_0_3" \in [1, oo)]] | "BeginLoop_1_2_1" \in [1, oo)] | "BeginLoop_2_2_3" \in [1, oo)]]] | "BeginLoop_2_2_0" \in [1, oo)]]] | "BeginLoop_0_2_3" \in [1, oo)] | "BeginLoop_2_0_1" \in [1, oo)] | "BeginLoop_2_0_2" \in [1, oo)]]]] | "BeginLoop_1_0_1" \in [1, oo)]]] | "BeginLoop_1_2_0" \in [1, oo)] | "BeginLoop_3_2_2" \in [1, oo)] | "BeginLoop_1_2_2" \in [1, oo)]] | "BeginLoop_3_0_2" \in [1, oo)] | "BeginLoop_0_1_2" \in [1, oo)]] | "BeginLoop_0_2_2" \in [1, oo)] | "BeginLoop_0_2_1" \in [1, oo)] | "BeginLoop_3_1_3" \in [1, oo)]]]] | "BeginLoop_2_1_1" \in [1, oo)] | "BeginLoop_0_0_1" \in [1, oo)] | "BeginLoop_3_2_3" \in [1, oo)]] | "BeginLoop_3_0_0" \in [1, oo)]] | "BeginLoop_3_2_1" \in [1, oo)] | "BeginLoop_2_0_3" \in [1, oo)] | "BeginLoop_1_1_0" \in [1, oo)] | "BeginLoop_2_2_1" \in [1, oo)]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | ["TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "TestTurn_2_2" \in [1, oo) | ["TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | ["TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | ["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | [["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)]]] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)]]]]]]]] & ~ [[["BeginLoop_3_0_3" \in [1, oo) | [[[["BeginLoop_1_1_1" \in [1, oo) | [[[["BeginLoop_3_2_1" \in [1, oo) | ["BeginLoop_0_1_0" \in [1, oo) | [[[[["BeginLoop_2_1_1" \in [1, oo) | [[["BeginLoop_1_0_2" \in [1, oo) | [["BeginLoop_0_2_1" \in [1, oo) | ["BeginLoop_0_2_2" \in [1, oo) | ["BeginLoop_0_0_2" \in [1, oo) | ["BeginLoop_0_1_2" \in [1, oo) | [[[["BeginLoop_3_2_2" \in [1, oo) | [[["BeginLoop_0_2_0" \in [1, oo) | ["BeginLoop_1_0_1" \in [1, oo) | [[[[[["BeginLoop_0_2_3" \in [1, oo) | ["BeginLoop_2_0_0" \in [1, oo) | [[[[["BeginLoop_2_2_3" \in [1, oo) | ["BeginLoop_1_2_1" \in [1, oo) | ["BeginLoop_2_1_0" \in [1, oo) | ["BeginLoop_1_0_3" \in [1, oo) | "BeginLoop_0_0_3" \in [1, oo)]]]] | "BeginLoop_1_2_3" \in [1, oo)] | "BeginLoop_3_0_1" \in [1, oo)] | "BeginLoop_2_2_0" \in [1, oo)] | "BeginLoop_3_1_0" \in [1, oo)]]] | "BeginLoop_2_0_1" \in [1, oo)] | "BeginLoop_2_0_2" \in [1, oo)] | "BeginLoop_0_1_1" \in [1, oo)] | "BeginLoop_3_2_0" \in [1, oo)] | "BeginLoop_0_0_0" \in [1, oo)]]] | "BeginLoop_2_1_3" \in [1, oo)] | "BeginLoop_1_2_0" \in [1, oo)]] | "BeginLoop_1_2_2" \in [1, oo)] | "BeginLoop_1_0_0" \in [1, oo)] | "BeginLoop_3_0_2" \in [1, oo)]]]]] | "BeginLoop_3_1_3" \in [1, oo)]] | "BeginLoop_3_1_1" \in [1, oo)] | "BeginLoop_3_1_2" \in [1, oo)]] | "BeginLoop_0_0_1" \in [1, oo)] | "BeginLoop_3_2_3" \in [1, oo)] | "BeginLoop_2_2_2" \in [1, oo)] | "BeginLoop_3_0_0" \in [1, oo)]]] | "BeginLoop_2_0_3" \in [1, oo)] | "BeginLoop_1_1_0" \in [1, oo)] | "BeginLoop_2_2_1" \in [1, oo)]] | "BeginLoop_1_1_2" \in [1, oo)] | "BeginLoop_1_1_3" \in [1, oo)] | "BeginLoop_0_1_3" \in [1, oo)]] | "BeginLoop_2_1_2" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[~ [["BeginLoop_2_1_2" \in [1, oo) | [["BeginLoop_0_1_3" \in [1, oo) | ["BeginLoop_1_1_3" \in [1, oo) | ["BeginLoop_1_1_2" \in [1, oo) | [["BeginLoop_2_2_1" \in [1, oo) | ["BeginLoop_1_1_0" \in [1, oo) | ["BeginLoop_2_0_3" \in [1, oo) | [[["BeginLoop_3_0_0" \in [1, oo) | ["BeginLoop_2_2_2" \in [1, oo) | ["BeginLoop_3_2_3" \in [1, oo) | ["BeginLoop_0_0_1" \in [1, oo) | [["BeginLoop_3_1_2" \in [1, oo) | ["BeginLoop_3_1_1" \in [1, oo) | [["BeginLoop_3_1_3" \in [1, oo) | [[[[["BeginLoop_3_0_2" \in [1, oo) | ["BeginLoop_1_0_0" \in [1, oo) | ["BeginLoop_1_2_2" \in [1, oo) | [["BeginLoop_1_2_0" \in [1, oo) | ["BeginLoop_2_1_3" \in [1, oo) | [[["BeginLoop_0_0_0" \in [1, oo) | ["BeginLoop_3_2_0" \in [1, oo) | ["BeginLoop_0_1_1" \in [1, oo) | ["BeginLoop_2_0_2" \in [1, oo) | ["BeginLoop_2_0_1" \in [1, oo) | [[["BeginLoop_3_1_0" \in [1, oo) | ["BeginLoop_2_2_0" \in [1, oo) | ["BeginLoop_3_0_1" \in [1, oo) | ["BeginLoop_1_2_3" \in [1, oo) | [[[["BeginLoop_0_0_3" \in [1, oo) | "BeginLoop_1_0_3" \in [1, oo)] | "BeginLoop_2_1_0" \in [1, oo)] | "BeginLoop_1_2_1" \in [1, oo)] | "BeginLoop_2_2_3" \in [1, oo)]]]]] | "BeginLoop_2_0_0" \in [1, oo)] | "BeginLoop_0_2_3" \in [1, oo)]]]]]] | "BeginLoop_1_0_1" \in [1, oo)] | "BeginLoop_0_2_0" \in [1, oo)]]] | "BeginLoop_3_2_2" \in [1, oo)]]]] | "BeginLoop_0_1_2" \in [1, oo)] | "BeginLoop_0_0_2" \in [1, oo)] | "BeginLoop_0_2_2" \in [1, oo)] | "BeginLoop_0_2_1" \in [1, oo)]] | "BeginLoop_1_0_2" \in [1, oo)]]] | "BeginLoop_2_1_1" \in [1, oo)]]]]] | "BeginLoop_0_1_0" \in [1, oo)] | "BeginLoop_3_2_1" \in [1, oo)]]]] | "BeginLoop_1_1_1" \in [1, oo)]]]] | "BeginLoop_3_0_3" \in [1, oo)]]] & [[[[[[[["TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo) | [[["TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo) | "TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)] | "TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)]] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo)] | "TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "TestTurn_2_2" \in [1, oo)] | "TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo)] | "TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m14sec

checking: ~ [EF [[["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | ["TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo) | ["TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo) | ["TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | ["TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | ["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | ["TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo) | ["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["Turn_0_3" \in [1, oo) && "TestTurn_3_0" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "TestTurn_0_2" \in [1, oo) | "TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)]]]]]]]]]]] & ["AskForSection_3_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_3_1" \in [1, oo) | ["AskForSection_1_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_0_2" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["AskForSection_2_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_3_0" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["AskForSection_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["AskForSection_2_2" \in [1, oo) && "Turn_2_1" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_3_0" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_0_2" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["AskForSection_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["AskForSection_1_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["AskForSection_0_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["AskForSection_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["AskForSection_3_2" \in [1, oo) && "Turn_2_0" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["Turn_1_3" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["AskForSection_2_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["AskForSection_1_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | ["AskForSection_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["Turn_1_3" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_3_1" \in [1, oo) | ["AskForSection_2_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | "Turn_0_2" \in [1, oo) && "AskForSection_3_0" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]
normalized: ~ [E [true U [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Turn_0_2" \in [1, oo) && "AskForSection_3_0" \in [1, oo) | "AskForSection_2_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_3_1" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "Turn_1_3" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "AskForSection_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "AskForSection_1_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "AskForSection_2_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "Turn_1_3" \in [1, oo) && "AskForSection_1_1" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "AskForSection_3_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "AskForSection_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_1_1" \in [1, oo)] | "AskForSection_0_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "AskForSection_1_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "AskForSection_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_3_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "AskForSection_2_2" \in [1, oo) && "Turn_2_1" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "AskForSection_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_3_0" \in [1, oo)] | "AskForSection_2_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "AskForSection_1_0" \in [1, oo) && "Turn_0_2" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_3_1" \in [1, oo)] | "AskForSection_3_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] & [[[[[[[[[[["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "Turn_2_0" \in [1, oo) && "TestTurn_0_2" \in [1, oo)] | "Turn_0_3" \in [1, oo) && "TestTurn_3_0" \in [1, oo)] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo)] | "TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo)] | "TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo)] | "TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo)] | "TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo)]]]]


before gc: list nodes free: 538435

after gc: idd nodes used:110939, unused:15889061; list nodes free:70819085
-> the formula is FALSE

FORMULA p_48_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m49sec

checking: ~ [EF [[[["AskForSection_3_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | ["Turn_0_2" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_0_2" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["AskForSection_2_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | ["AskForSection_2_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_3_0" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["AskForSection_3_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_0_2" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["AskForSection_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["AskForSection_1_2" \in [1, oo) && "Turn_2_0" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["Turn_1_0" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["AskForSection_0_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["AskForSection_1_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | ["AskForSection_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["AskForSection_2_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | ["AskForSection_1_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["Turn_1_0" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["AskForSection_1_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | [[["AskForSection_0_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | [[["Turn_1_2" \in [1, oo) && "AskForSection_3_1" \in [1, oo) | ["AskForSection_2_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | "Turn_0_2" \in [1, oo) && "AskForSection_3_0" \in [1, oo)]] | "Turn_2_2" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "AskForSection_0_2" \in [1, oo) && "Turn_2_1" \in [1, oo)]] | "Turn_2_1" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_1_0" \in [1, oo) && "AskForSection_0_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Turn_1_0" \in [1, oo) && "AskForSection_3_1" \in [1, oo)] | [["TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo) | [[["TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | [[["TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo) | ["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | [["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)]]] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)]] | "TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo)] | "TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo)]] | "TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo)]]]]
normalized: ~ [E [true U [["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | [["TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo) | ["TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | [["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | [[["TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo) | "TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)]] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)]]] | "TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo)]]] | "TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo)]] | ["Turn_1_0" \in [1, oo) && "AskForSection_3_1" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[["Turn_1_0" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | [["AskForSection_0_2" \in [1, oo) && "Turn_2_1" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | [["Turn_0_2" \in [1, oo) && "AskForSection_3_0" \in [1, oo) | "AskForSection_2_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_3_1" \in [1, oo)]]] | "AskForSection_0_1" \in [1, oo) && "Turn_1_3" \in [1, oo)]]] | "Turn_0_1" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "AskForSection_1_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_1_0" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "AskForSection_1_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "AskForSection_2_1" \in [1, oo) && "Turn_1_1" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "AskForSection_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "AskForSection_1_1" \in [1, oo) && "Turn_1_2" \in [1, oo)] | "AskForSection_0_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_1_0" \in [1, oo) && "AskForSection_1_1" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "AskForSection_1_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "AskForSection_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "AskForSection_3_0" \in [1, oo) && "Turn_0_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_1_1" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_3_0" \in [1, oo)] | "AskForSection_2_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "AskForSection_2_2" \in [1, oo) && "Turn_2_3" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "AskForSection_3_1" \in [1, oo) && "Turn_1_1" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_49_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m12sec

checking: ~ [EF [[[["Turn_1_1" \in [1, oo) && "AskForSection_3_1" \in [1, oo) | [[["Turn_2_1" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | [["Turn_0_2" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | [["AskForSection_2_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_3_0" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | [[[["Turn_2_3" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["AskForSection_3_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | [[["Turn_0_2" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_0_0" \in [1, oo) | ["AskForSection_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_2_0" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_1_2" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_3" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["Turn_1_0" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["AskForSection_0_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["AskForSection_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["Turn_1_1" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["AskForSection_1_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_1_2" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["Turn_1_0" \in [1, oo) && "AskForSection_2_1" \in [1, oo) | ["AskForSection_1_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["AskForSection_0_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | ["Turn_0_1" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | ["Turn_1_0" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_3_2" \in [1, oo) | ["AskForSection_0_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | ["Turn_2_2" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["AskForSection_3_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | ["AskForSection_2_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | "AskForSection_3_0" \in [1, oo) && "Turn_0_2" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]]]]] | "Turn_2_0" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_0_1" \in [1, oo)]]] | "Turn_2_1" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_1_1" \in [1, oo)]]]] | "Turn_2_3" \in [1, oo) && "AskForSection_2_2" \in [1, oo)]]] | "Turn_2_2" \in [1, oo) && "AskForSection_0_2" \in [1, oo)]]] | "Turn_0_0" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "AskForSection_1_0" \in [1, oo) && "Turn_0_2" \in [1, oo)]] | "Turn_1_0" \in [1, oo) && "AskForSection_3_1" \in [1, oo)] & ~ [[[[["TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo) | [["TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo) | [[[["TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo) | ["TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo) | "TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo)]] | "TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo)] | "TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo)] | "TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo)]] | "TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo)]] | "TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo)] | "TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo)] | "TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo)]]]]]
normalized: ~ [E [true U [~ [["TestTurn_0_0" \in [1, oo) && "Turn_0_0" \in [1, oo) | ["TestTurn_1_0" \in [1, oo) && "Turn_0_1" \in [1, oo) | ["TestTurn_2_2" \in [1, oo) && "Turn_2_2" \in [1, oo) | [["TestTurn_2_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | [["TestTurn_2_1" \in [1, oo) && "Turn_1_2" \in [1, oo) | ["TestTurn_1_2" \in [1, oo) && "Turn_2_1" \in [1, oo) | ["TestTurn_0_1" \in [1, oo) && "Turn_1_0" \in [1, oo) | [["TestTurn_1_1" \in [1, oo) && "Turn_1_1" \in [1, oo) | "TestTurn_0_2" \in [1, oo) && "Turn_2_0" \in [1, oo)] | "TestTurn_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)]]]] | "TestTurn_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)]] | "TestTurn_3_2" \in [1, oo) && "Turn_2_3" \in [1, oo)]]]]] & ["Turn_1_0" \in [1, oo) && "AskForSection_3_1" \in [1, oo) | [["AskForSection_1_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | ["Turn_0_0" \in [1, oo) && "AskForSection_1_0" \in [1, oo) | [[["Turn_2_2" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | [[["Turn_2_3" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | [[[["Turn_1_1" \in [1, oo) && "AskForSection_1_1" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | ["Turn_2_1" \in [1, oo) && "AskForSection_2_2" \in [1, oo) | [[["Turn_1_2" \in [1, oo) && "AskForSection_0_1" \in [1, oo) | ["Turn_2_0" \in [1, oo) && "AskForSection_0_2" \in [1, oo) | [[[[[[[[[[[[[[[[[[[[[[[[[[["AskForSection_3_0" \in [1, oo) && "Turn_0_2" \in [1, oo) | "AskForSection_2_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "AskForSection_3_1" \in [1, oo) && "Turn_1_2" \in [1, oo)] | "Turn_2_2" \in [1, oo) && "AskForSection_2_2" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_0_2" \in [1, oo)] | "AskForSection_0_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_1_0" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_1_0" \in [1, oo)] | "AskForSection_0_2" \in [1, oo) && "Turn_2_3" \in [1, oo)] | "AskForSection_1_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_1_0" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "AskForSection_1_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_2_1" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "AskForSection_3_1" \in [1, oo) && "Turn_1_3" \in [1, oo)] | "Turn_1_2" \in [1, oo) && "AskForSection_1_1" \in [1, oo)] | "AskForSection_0_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_1_0" \in [1, oo) && "AskForSection_1_1" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_1_1" \in [1, oo) && "AskForSection_0_1" \in [1, oo)] | "Turn_2_0" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "AskForSection_3_0" \in [1, oo) && "Turn_0_3" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_0_0" \in [1, oo) && "AskForSection_0_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_2_0" \in [1, oo)]]] | "AskForSection_3_0" \in [1, oo) && "Turn_0_0" \in [1, oo)] | "Turn_2_3" \in [1, oo) && "AskForSection_1_2" \in [1, oo)]]]] | "Turn_2_2" \in [1, oo) && "AskForSection_3_2" \in [1, oo)] | "Turn_0_1" \in [1, oo) && "AskForSection_3_0" \in [1, oo)] | "AskForSection_2_1" \in [1, oo) && "Turn_1_3" \in [1, oo)]] | "Turn_0_0" \in [1, oo) && "AskForSection_2_0" \in [1, oo)] | "Turn_0_2" \in [1, oo) && "AskForSection_0_0" \in [1, oo)]] | "Turn_2_2" \in [1, oo) && "AskForSection_1_2" \in [1, oo)] | "Turn_2_1" \in [1, oo) && "AskForSection_1_2" \in [1, oo)]]] | "Turn_1_1" \in [1, oo) && "AskForSection_3_1" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_50_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m34sec


total processing time: 3m24sec

STOP 1369682730

--------------------
content from stderr:

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

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

initing FirstDep: 0m0sec


iterations count:593 (1), effective:58 (0)
51127 52862 54707 55771 55183 55819
iterations count:6238 (18), effective:184 (0)

iterations count:593 (1), effective:58 (0)
51127 52862 54707 55771 55183 55819
iterations count:6238 (18), effective:184 (0)
66292
iterations count:1640 (4), effective:74 (0)
54868 54088 53354 51372 51134 56143 56854 56303 56582 57162 57132 57484 57209 56559 56652 56485
iterations count:16891 (50), effective:468 (1)

iterations count:957 (2), effective:23 (0)
47484 50212 50861 51850 53265 53345 52673 51556 50282 55835 56023 55705 56324 56324 56976 57020 57352 56361 56629 56876 56300
iterations count:21747 (65), effective:561 (1)

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