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=DrinkVendingMachine-PT-02
export BK_EXAMINATION=ReachabilityFireability
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1659
export BIN_DIR=/home/mcc/BenchKit/bin
BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/DrinkVendingMachine-PT-02
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is DrinkVendingMachine-PT-02, examination is ReachabilityFireability'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo 'START 1369384248'

Execution Outputs of marcie for DrinkVendingMachine/02 (P/T)

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

execution on node 34: cluster1u36.lip6.fr (runId=136937309300839_n_34)
=====================================================================
runnning marcie on DrinkVendingMachine-PT-02 (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 DrinkVendingMachine-PT-02, examination is ReachabilityFireability
=====================================================================

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

START 1369384248

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: 24 NrTr: 72)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m1sec


RS generation: 0m0sec


-> reachability set: #nodes 34 (3.4e+01) #states 1,024 (3)



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

checking: AG [[["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)] & ["theOptions_2" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo) | ["theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) | "theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo)]]]]]]]]]
normalized: ~ [E [true U ~ [[["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)] & [[[[[[["theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo) | "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) && "theOptions_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo)] | "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo) && "theOptions_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)] | ["theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo) | [[["theOptions_2" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) | "theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo)]] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo)]]]]]]
normalized: ~ [E [true U ~ [[["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)] | ["theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo) | [[["theOptions_2" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) | ["theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo) | "theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo)]] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo)]]]]]]]]

-> the formula is FALSE

FORMULA p_3_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["theProducts_2" \in [1, oo) && "wait_3" \in [1, oo) && "theOptions_2" \in [1, oo) | [[[["wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo) | ["theProducts_1" \in [1, oo) && "wait_4" \in [1, oo) && "theOptions_1" \in [1, oo) | "theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo)]]] | "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo)]] & ~ [["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[~ [["productSlots_1" \in [1, oo) | "productSlots_2" \in [1, oo)]] & [["theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) | [[["theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_3" \in [1, oo) | "theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_4" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)]]]] | "theOptions_2" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_3" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)]] | ["wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [1, oo) | [[["theProducts_2" \in [1, oo) && "wait_4" \in [1, oo) && "theOptions_2" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo) | [["wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) | "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo)] | "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo)]]] | "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo)] | "theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)]]]]
normalized: ~ [E [true U ~ [[[["theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) | [[["theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)]] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theProducts_2" \in [1, oo) && "wait_4" \in [1, oo)]]] | "theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)] | ~ [["productSlots_1" \in [1, oo) | "productSlots_2" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[["productSlots_2" \in [1, oo) | "productSlots_1" \in [1, oo)] <-> ["wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [1, oo) | ["wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) | ["wait_3" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) | "theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)]]]]]]]]]
normalized: ~ [E [true U ~ [[[~ [[[[[[[["theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)]] & ~ [["productSlots_1" \in [1, oo) | "productSlots_2" \in [1, oo)]]] | [["productSlots_1" \in [1, oo) | "productSlots_2" \in [1, oo)] & [[[[[[["theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [1, oo) && "wait_4" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [1, oo) && "wait_3" \in [1, oo) && "theProducts_2" \in [1, oo)]]]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[["wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) | [[["wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo) | ["wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo) | [[["wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo) | [[[[["wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [2, oo)] | "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo)]] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)]]]] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo)]] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] & ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [3, oo) | ["theOptions_2" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | [[[["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | [[["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | [["theProducts_1" \in [1, oo) && "wait_8" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | [[[["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | [["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_1" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | [[[["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)]]] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "theOptions_2" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)]]]] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo)]]]]]] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [1, oo)]] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)]] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [1, oo)]]] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)]]]]]]]
normalized: ~ [E [true U [[[[["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | [[["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | [["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | [["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | [[[[[["theOptions_2" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | [[[["theOptions_2" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | [[["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)]]]] | "theOptions_1" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)]] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo)]]]] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "theProducts_1" \in [1, oo) && "wait_8" \in [1, oo)]] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)]]] | "theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo)]]]] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)] & ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | [["theOptions_1" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | [[[["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | [["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_1" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)]]]]] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)]]] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo)]]] | "theOptions_1" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo)]]]]]

-> the formula is TRUE

FORMULA p_48_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[[["wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) | ["wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) | ["wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) | [[[[[[[[[[["wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)]]]] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | [[[[[[[[[[[[[[[[[[[[[[[["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [3, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [3, oo) | [[[[[["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo)]]] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [3, oo)]]]]
normalized: ~ [E [true U [["theOptions_1" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | [[["theOptions_2" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo)]]]]]] | "theOptions_1" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo)]]]]]]]]]]]]]]]]]]]]]]]] | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | [[[["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_1" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)]]]]]]]]]]] | "theOptions_1" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_1" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_1" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo)]]]]]

-> the formula is FALSE

FORMULA p_49_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[~ [[[[[[[[[[[[[[["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | [[[[[[[[[[[[[[[["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [3, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [3, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo)]]] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [3, oo)] | "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [3, oo)]] & ~ [[[[[[[[[[[[[[[["wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)]]]]]
normalized: ~ [E [true U [~ [[[[[[[[[[[[[[["theOptions_2" \in [2, oo) && "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo) | "theOptions_1" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)]] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [2, oo) && "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "wait_5" \in [1, oo) && "theProducts_1" \in [1, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)] | "wait_6" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_6" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo)] | "wait_5" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [1, oo)]] & ~ [["theOptions_1" \in [3, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_1" \in [3, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) | ["theOptions_2" \in [2, oo) && "theOptions_1" \in [1, oo) && "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) | [[["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [3, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [3, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_2" \in [3, oo) | ["wait_8" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo) | ["wait_7" \in [1, oo) && "theProducts_2" \in [1, oo) && "theOptions_2" \in [3, oo) | ["wait_7" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [1, oo) && "theOptions_2" \in [2, oo) | "wait_8" \in [1, oo) && "theProducts_1" \in [1, oo) && "theOptions_1" \in [2, oo) && "theOptions_2" \in [1, oo)]]]]]]]]]]]]]]]] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_7" \in [1, oo) && "theProducts_1" \in [1, oo)] | "theOptions_2" \in [1, oo) && "theOptions_1" \in [2, oo) && "wait_8" \in [1, oo) && "theProducts_2" \in [1, oo)]]]]]]]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_50_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 0m2sec

STOP 1369384250

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


iterations count:324 (4), effective:28 (0)

initing FirstDep: 0m0sec


iterations count:78 (1), effective:3 (0)

iterations count:132 (1), effective:11 (0)

iterations count:75 (1), effective:2 (0)

iterations count:109 (1), effective:11 (0)

iterations count:78 (1), effective:3 (0)

iterations count:97 (1), effective:4 (0)

iterations count:84 (1), effective:5 (0)

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