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

Execution Outputs of marcie for SharedMemory/000100 (P/T)

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

execution on node 3: quadhexa-2.u-paris10.fr (runId=136983895600239_n_3)
=====================================================================
runnning marcie on SharedMemory-PT-000100 (CTLMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is SharedMemory-PT-000100, examination is CTLMix
=====================================================================

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

START 1369871658

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 10301 NrTr: 20100)

net check time: 0m0sec

CANNOT_COMPUTE

STOP 1369871670

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

mcc/mcc_parse.cc:759: Exception: parse error ctl p_1880_mix_eq_x: E F (X (true & (|marking(Memory_17)|=|marking(OwnMemAcc_17)|) & (|marking(Memory_67)|=|marking(OwnMemAcc_67)|) & (|marking(Memory_88)|=|marking(OwnMemAcc_88)|) & (|marking(Memory_77)|=|marking(OwnMemAcc_77)|) & (|marking(Memory_33)|=|marking(OwnMemAcc_33)|) & (|marking(Memory_30)|=|marking(OwnMemAcc_30)|) & (|marking(Memory_45)|=|marking(OwnMemAcc_45)|) & (|marking(Memory_23)|=|marking(OwnMemAcc_23)|) & (|marking(Memory_61)|=|marking(OwnMemAcc_61)|) & (|marking(Memory_66)|=|marking(OwnMemAcc_66)|) & (|marking(Memory_73)|=|marking(OwnMemAcc_73)|) & (|marking(Memory_5)|=|marking(OwnMemAcc_5)|) & (|marking(Memory_16)|=|marking(OwnMemAcc_16)|) & (|marking(Memory_34)|=|marking(OwnMemAcc_34)|) & (|marking(Memory_1)|=|marking(OwnMemAcc_1)|) & (|marking(Memory_13)|=|marking(OwnMemAcc_13)|) & (|marking(Memory_9)|=|marking(OwnMemAcc_9)|) & (|marking(Memory_97)|=|marking(OwnMemAcc_97)|) & (|marking(Memory_87)|=|marking(OwnMemAcc_87)|) & (|marking(Memory_96)|=|marking(OwnMemAcc_96)|) & (|marking(Memory_25)|=|marking(OwnMemAcc_25)|) & (|marking(Memory_72)|=|marking(OwnMemAcc_72)|) & (|marking(Memory_38)|=|marking(OwnMemAcc_38)|) & (|marking(Memory_93)|=|marking(OwnMemAcc_93)|) & (|marking(Memory_10)|=|marking(OwnMemAcc_10)|) & (|marking(Memory_51)|=|marking(OwnMemAcc_51)|) & (|marking(Memory_8)|=|marking(OwnMemAcc_8)|) & (|marking(Memory_55)|=|marking(OwnMemAcc_55)|) & (|marking(Memory_54)|=|marking(OwnMemAcc_54)|) & (|marking(Memory_14)|=|marking(OwnMemAcc_14)|) & (|marking(Memory_62)|=|marking(OwnMemAcc_62)|) & (|marking(Memory_43)|=|marking(OwnMemAcc_43)|) & (|marking(Memory_36)|=|marking(OwnMemAcc_36)|) & (|marking(Memory_60)|=|marking(OwnMemAcc_60)|) & (|marking(Memory_18)|=|marking(OwnMemAcc_18)|) & (|marking(Memory_76)|=|marking(OwnMemAcc_76)|) & (|marking(Memory_42)|=|marking(OwnMemAcc_42)|) & (|marking(Memory_75)|=|marking(OwnMemAcc_75)|) & (|marking(Memory_3)|=|marking(OwnMemAcc_3)|) & (|marking(Memory_31)|=|marking(OwnMemAcc_31)|) & (|marking(Memory_2)|=|marking(OwnMemAcc_2)|) & (|marking(Memory_86)|=|marking(OwnMemAcc_86)|) & (|marking(Memory_64)|=|marking(OwnMemAcc_64)|) & (|marking(Memory_85)|=|marking(OwnMemAcc_85)|) & (|marking(Memory_15)|=|marking(OwnMemAcc_15)|) & (|marking(Memory_84)|=|marking(OwnMemAcc_84)|) & (|marking(Memory_91)|=|marking(OwnMemAcc_91)|) & (|marking(Memory_57)|=|marking(OwnMemAcc_57)|) & (|marking(Memory_99)|=|marking(OwnMemAcc_99)|) & (|marking(Memory_7)|=|marking(OwnMemAcc_7)|) & (|marking(Memory_28)|=|marking(OwnMemAcc_28)|) & (|marking(Memory_27)|=|marking(OwnMemAcc_27)|) & (|marking(Memory_19)|=|marking(OwnMemAcc_19)|) & (|marking(Memory_6)|=|marking(OwnMemAcc_6)|) & (|marking(Memory_70)|=|marking(OwnMemAcc_70)|) & (|marking(Memory_71)|=|marking(OwnMemAcc_71)|) & (|marking(Memory_46)|=|marking(OwnMemAcc_46)|) & (|marking(Memory_69)|=|marking(OwnMemAcc_69)|) & (|marking(Memory_39)|=|marking(OwnMemAcc_39)|) & (|marking(Memory_89)|=|marking(OwnMemAcc_89)|) & (|marking(Memory_22)|=|marking(OwnMemAcc_22)|) & (|marking(Memory_4)|=|marking(OwnMemAcc_4)|) & (|marking(Memory_56)|=|marking(OwnMemAcc_56)|) & (|marking(Memory_20)|=|marking(OwnMemAcc_20)|) & (|marking(Memory_47)|=|marking(OwnMemAcc_47)|) & (|marking(Memory_74)|=|marking(OwnMemAcc_74)|) & (|marking(Memory_68)|=|marking(OwnMemAcc_68)|) & (|marking(Memory_95)|=|marking(OwnMemAcc_95)|) & (|marking(Memory_44)|=|marking(OwnMemAcc_44)|) & (|marking(Memory_80)|=|marking(OwnMemAcc_80)|) & (|marking(Memory_21)|=|marking(OwnMemAcc_21)|) & (|marking(Memory_12)|=|marking(OwnMemAcc_12)|) & (|marking(Memory_53)|=|marking(OwnMemAcc_53)|) & (|marking(Memory_59)|=|marking(OwnMemAcc_59)|) & (|marking(Memory_100)|=|marking(OwnMemAcc_100)|) & (|marking(Memory_24)|=|marking(OwnMemAcc_24)|) & (|marking(Memory_82)|=|marking(OwnMemAcc_82)|) & (|marking(Memory_26)|=|marking(OwnMemAcc_26)|) & (|marking(Memory_81)|=|marking(OwnMemAcc_81)|) & (|marking(Memory_50)|=|marking(OwnMemAcc_50)|) & (|marking(Memory_35)|=|marking(OwnMemAcc_35)|) & (|marking(Memory_37)|=|marking(OwnMemAcc_37)|) & (|marking(Memory_94)|=|marking(OwnMemAcc_94)|) & (|marking(Memory_78)|=|marking(OwnMemAcc_78)|) & (|marking(Memory_58)|=|marking(OwnMemAcc_58)|) & (|marking(Memory_65)|=|marking(OwnMemAcc_65)|) & (|marking(Memory_83)|=|marking(OwnMemAcc_83)|) & (|marking(Memory_49)|=|marking(OwnMemAcc_49)|) & (|marking(Memory_92)|=|marking(OwnMemAcc_92)|) & (|marking(Memory_98)|=|marking(OwnMemAcc_98)|) & (|marking(Memory_48)|=|marking(OwnMemAcc_48)|) & (|marking(Memory_11)|=|marking(OwnMemAcc_11)|) & (|marking(Memory_79)|=|marking(OwnMemAcc_79)|) & (|marking(Memory_29)|=|marking(OwnMemAcc_29)|) & (|marking(Memory_90)|=|marking(OwnMemAcc_90)|) & (|marking(Memory_52)|=|marking(OwnMemAcc_52)|) & (|marking(Memory_41)|=|marking(OwnMemAcc_41)|) & (|marking(Memory_40)|=|marking(OwnMemAcc_40)|) & (|marking(Memory_32)|=|marking(OwnMemAcc_32)|) & (|marking(Memory_63)|=|marking(OwnMemAcc_63)|)) & E G ((|marking(OwnMemAcc_60)|+|marking(OwnMemAcc_31)|+|marking(OwnMemAcc_77)|+|marking(OwnMemAcc_7)|+|marking(OwnMemAcc_76)|+|marking(OwnMemAcc_71)|+|marking(OwnMemAcc_21)|+|marking(OwnMemAcc_26)|+|marking(OwnMemAcc_33)|+|marking(OwnMemAcc_85)|+|marking(OwnMemAcc_97)|+|marking(OwnMemAcc_30)|+|marking(OwnMemAcc_12)|+|marking(OwnMemAcc_84)|+|marking(OwnMemAcc_29)|+|marking(OwnMemAcc_47)|+|marking(OwnMemAcc_8)|+|marking(OwnMemAcc_45)|+|marking(OwnMemAcc_98)|+|marking(OwnMemAcc_99)|+|marking(OwnMemAcc_58)|+|marking(OwnMemAcc_3)|+|marking(OwnMemAcc_40)|+|marking(OwnMemAcc_46)|+|marking(OwnMemAcc_89)|+|marking(OwnMemAcc_69)|+|marking(OwnMemAcc_53)|+|marking(OwnMemAcc_38)|+|marking(OwnMemAcc_61)|+|marking(OwnMemAcc_15)|+|marking(OwnMemAcc_43)|+|marking(OwnMemAcc_59)|+|marking(OwnMemAcc_52)|+|marking(OwnMemAcc_70)|+|marking(OwnMemAcc_96)|+|marking(OwnMemAcc_49)|+|marking(OwnMemAcc_65)|+|marking(OwnMemAcc_48)|+|marking(OwnMemAcc_92)|+|marking(OwnMemAcc_32)|+|marking(OwnMemAcc_80)|+|marking(OwnMemAcc_82)|+|marking(OwnMemAcc_16)|+|marking(OwnMemAcc_11)|+|marking(OwnMemAcc_62)|+|marking(OwnMemAcc_87)|+|marking(OwnMemAcc_72)|+|marking(OwnMemAcc_39)|+|marking(OwnMemAcc_56)|+|marking(OwnMemAcc_93)|+|marking(OwnMemAcc_27)|+|marking(OwnMemAcc_41)|+|marking(OwnMemAcc_51)|+|marking(OwnMemAcc_83)|+|marking(OwnMemAcc_74)|+|marking(OwnMemAcc_73)|+|marking(OwnMemAcc_100)|+|marking(OwnMemAcc_44)|+|marking(OwnMemAcc_63)|+|marking(OwnMemAcc_2)|+|marking(OwnMemAcc_68)|+|marking(OwnMemAcc_67)|+|marking(OwnMemAcc_50)|+|marking(OwnMemAcc_54)|+|marking(OwnMemAcc_19)|+|marking(OwnMemAcc_17)|+|marking(OwnMemAcc_10)|+|marking(OwnMemAcc_42)|+|marking(OwnMemAcc_34)|+|marking(OwnMemAcc_22)|+|marking(OwnMemAcc_94)|+|marking(OwnMemAcc_4)|+|marking(OwnMemAcc_23)|+|marking(OwnMemAcc_13)|+|marking(OwnMemAcc_90)|+|marking(OwnMemAcc_35)|+|marking(OwnMemAcc_57)|+|marking(OwnMemAcc_88)|+|marking(OwnMemAcc_37)|+|marking(OwnMemAcc_36)|+|marking(OwnMemAcc_6)|+|marking(OwnMemAcc_64)|+|marking(OwnMemAcc_81)|+|marking(OwnMemAcc_66)|+|marking(OwnMemAcc_91)|+|marking(OwnMemAcc_1)|+|marking(OwnMemAcc_20)|+|marking(OwnMemAcc_95)|+|marking(OwnMemAcc_28)|+|marking(OwnMemAcc_9)|+|marking(OwnMemAcc_25)|+|marking(OwnMemAcc_75)|+|marking(OwnMemAcc_18)|+|marking(OwnMemAcc_55)|+|marking(OwnMemAcc_14)|+|marking(OwnMemAcc_78)|+|marking(OwnMemAcc_24)|+|marking(OwnMemAcc_79)|+|marking(OwnMemAcc_86)|+|marking(OwnMemAcc_5)|)!=(|marking(Active_75)|+|marking(Active_60)|+|marking(Active_38)|+|marking(Active_84)|+|marking(Active_81)|+|marking(Active_4)|+|marking(Active_6)|+|marking(Active_68)|+|marking(Active_55)|+|marking(Active_74)|+|marking(Active_99)|+|marking(Active_33)|+|marking(Active_14)|+|marking(Active_26)|+|marking(Active_50)|+|marking(Active_21)|+|marking(Active_82)|+|marking(Active_91)|+|marking(Active_95)|+|marking(Active_28)|+|marking(Active_90)|+|marking(Active_98)|+|marking(Active_77)|+|marking(Active_83)|+|marking(Active_76)|+|marking(Active_29)|+|marking(Active_63)|+|marking(Active_19)|+|marking(Active_30)|+|marking(Active_51)|+|marking(Active_56)|+|marking(Active_17)|+|marking(Active_65)|+|marking(Active_45)|+|marking(Active_11)|+|marking(Active_13)|+|marking(Active_42)|+|marking(Active_2)|+|marking(Active_34)|+|marking(Active_62)|+|marking(Active_12)|+|marking(Active_49)|+|marking(Active_53)|+|marking(Active_92)|+|marking(Active_79)|+|marking(Active_93)|+|marking(Active_20)|+|marking(Active_87)|+|marking(Active_85)|+|marking(Active_72)|+|marking(Active_67)|+|marking(Active_46)|+|marking(Active_59)|+|marking(Active_70)|+|marking(Active_25)|+|marking(Active_41)|+|marking(Active_97)|+|marking(Active_37)|+|marking(Active_73)|+|marking(Active_9)|+|marking(Active_96)|+|marking(Active_32)|+|marking(Active_52)|+|marking(Active_39)|+|marking(Active_5)|+|marking(Active_36)|+|marking(Active_15)|+|marking(Active_80)|+|marking(Active_23)|+|marking(Active_40)|+|marking(Active_71)|+|marking(Active_1)|+|marking(Active_86)|+|marking(Active_88)|+|marking(Active_18)|+|marking(Active_64)|+|marking(Active_3)|+|marking(Active_22)|+|marking(Active_43)|+|marking(Active_35)|+|marking(Active_44)|+|marking(Active_66)|+|marking(Active_31)|+|marking(Active_61)|+|marking(Active_89)|+|marking(Active_7)|+|marking(Active_16)|+|marking(Active_47)|+|marking(Active_54)|+|marking(Active_27)|+|marking(Active_24)|+|marking(Active_8)|+|marking(Active_100)|+|marking(Active_69)|+|marking(Active_58)|+|marking(Active_94)|+|marking(Active_78)|+|marking(Active_10)|+|marking(Active_48)|+|marking(Active_57)|)))
ctl p_1881_mix_full_and: E F ((Begin_Own_Acc_56? | Begin_Own_Acc_29? | Begin_Own_Acc_23? | Begin_Own_Acc_87? | Begin_Own_Acc_63? | Begin_Own_Acc_36? | Begin_Own_Acc_39? | Begin_Own_Acc_14? | Begin_Own_Acc_91? | Begin_Own_Acc_40? | Begin_Own_Acc_15? | Begin_Own_Acc_57? | Begin_Own_Acc_98? | Begin_Own_Acc_38? | Begin_Own_Acc_55? | Begin_Own_Acc_44? | Begin_Own_Acc_90? | Begin_Own_Acc_5? | Begin_Own_Acc_68? | Begin_Own_Acc_10? | Begin_Own_Acc_9? | Begin_Own_Acc_71? | Begin_Own_Acc_77? | Begin_Own_Acc_78? | Begin_Own_Acc_84? | Begin_Own_Acc_11? | Begin_Own_Acc_88? | Begin_Own_Acc_70? | Begin_Own_Acc_50? | Begin_Own_Acc_7? | Begin_Own_Acc_62? | Begin_Own_Acc_85? | Begin_Own_Acc_83? | Begin_Own_Acc_51? | Begin_Own_Acc_41? | Begin_Own_Acc_96? | Begin_Own_Acc_34? | Begin_Own_Acc_19? | Begin_Own_Acc_100? | Begin_Own_Acc_27? | Begin_Own_Acc_53? | Begin_Own_Acc_58? | Begin_Own_Acc_86? | Begin_Own_Acc_35? | Begin_Own_Acc_94? | Begin_Own_Acc_3? | Begin_Own_Acc_97? | Begin_Own_Acc_21? | Begin_Own_Acc_6? | Begin_Own_Acc_17? | Begin_Own_Acc_37? | Begin_Own_Acc_59? | Begin_Own_Acc_28? | Begin_Own_Acc_81? | Begin_Own_Acc_1? | Begin_Own_Acc_47? | Begin_Own_Acc_13? | Begin_Own_Acc_82? | Begin_Own_Acc_31? | Begin_Own_Acc_79? | Begin_Own_Acc_30? | Begin_Own_Acc_99? | Begin_Own_Acc_60? | Begin_Own_Acc_2? | Begin_Own_Acc_74? | Begin_Own_Acc_49? | Begin_Own_Acc_4? | Begin_Own_Acc_93? | Begin_Own_Acc_95? | Begin_Own_Acc_42? | Begin_Own_Acc_54? | Begin_Own_Acc_20? | Begin_Own_Acc_16? | Begin_Own_Acc_65? | Begin_Own_Acc_26? | Begin_Own_Acc_89? | Begin_Own_Acc_45? | Begin_Own_Acc_92? | Begin_Own_Acc_24? | Begin_Own_Acc_32? | Begin_Own_Acc_46? | Begin_Own_Acc_43? | Begin_Own_Acc_69? | Begin_Own_Acc_72? | Begin_Own_Acc_48? | Begin_Own_Acc_8? | Begin_Own_Acc_73? | Begin_Own_Acc_52? | Begin_Own_Acc_76? | Begin_Own_Acc_25? | Begin_Own_Acc_61? | Begin_Own_Acc_67? | Begin_Own_Acc_33? | Begin_Own_Acc_75? | Begin_Own_Acc_18? | Begin_Own_Acc_12? | Begin_Own_Acc_22? | Begin_Own_Acc_80? | Begin_Own_Acc_64? | Begin_Own_Acc_66?) & (Req_Ext_Acc_35? | Req_Ext_Acc_14? | Req_Ext_Acc_79? | Req_Ext_Acc_62? | Req_Ext_Acc_86? | Req_Ext_Acc_97? | Req_Ext_Acc_69? | Req_Ext_Acc_68? | Req_Ext_Acc_84? | Req_Ext_Acc_7? | Req_Ext_Acc_61? | Req_Ext_Acc_66? | Req_Ext_Acc_22? | Req_Ext_Acc_59? | Req_Ext_Acc_51? | Req_Ext_Acc_38? | Req_Ext_Acc_80? | Req_Ext_Acc_17? | Req_Ext_Acc_1? | Req_Ext_Acc_87? | Req_Ext_Acc_37? | Req_Ext_Acc_3? | Req_Ext_Acc_11? | Req_Ext_Acc_33? | Req_Ext_Acc_78? | Req_Ext_Acc_94? | Req_Ext_Acc_5? | Req_Ext_Acc_65? | Req_Ext_Acc_10? | Req_Ext_Acc_20? | Req_Ext_Acc_56? | Req_Ext_Acc_25? | Req_Ext_Acc_48? | Req_Ext_Acc_2? | Req_Ext_Acc_93? | Req_Ext_Acc_34? | Req_Ext_Acc_49? | Req_Ext_Acc_42? | Req_Ext_Acc_54? | Req_Ext_Acc_31? | Req_Ext_Acc_63? | Req_Ext_Acc_64? | Req_Ext_Acc_81? | Req_Ext_Acc_71? | Req_Ext_Acc_50? | Req_Ext_Acc_72? | Req_Ext_Acc_43? | Req_Ext_Acc_32? | Req_Ext_Acc_19? | Req_Ext_Acc_82? | Req_Ext_Acc_83? | Req_Ext_Acc_58? | Req_Ext_Acc_55? | Req_Ext_Acc_96? | Req_Ext_Acc_73? | Req_Ext_Acc_28? | Req_Ext_Acc_27? | Req_Ext_Acc_30? | Req_Ext_Acc_36? | Req_Ext_Acc_60? | Req_Ext_Acc_4? | Req_Ext_Acc_12? | Req_Ext_Acc_29? | Req_Ext_Acc_70? | Req_Ext_Acc_44? | Req_Ext_Acc_9? | Req_Ext_Acc_52? | Req_Ext_Acc_92? | Req_Ext_Acc_88? | Req_Ext_Acc_15? | Req_Ext_Acc_40? | Req_Ext_Acc_74? | Req_Ext_Acc_91? | Req_Ext_Acc_46? | Req_Ext_Acc_24? | Req_Ext_Acc_98? | Req_Ext_Acc_100? | Req_Ext_Acc_90? | Req_Ext_Acc_57? | Req_Ext_Acc_39? | Req_Ext_Acc_53? | Req_Ext_Acc_6? | Req_Ext_Acc_41? | Req_Ext_Acc_76? | Req_Ext_Acc_47? | Req_Ext_Acc_99? | Req_Ext_Acc_21? | Req_Ext_Acc_16? | Req_Ext_Acc_45? | Req_Ext_Acc_8? | Req_Ext_Acc_26? | Req_Ext_Acc_89? | Req_Ext_Acc_77? | Req_Ext_Acc_67? | Req_Ext_Acc_85? | Req_Ext_Acc_75? | Req_Ext_Acc_18? | Req_Ext_Acc_13? | Req_Ext_Acc_23? | Req_Ext_Acc_95?))
ctl p_1882_mix_full_or: A G ((Begin_Own_Acc_56? | Begin_Own_Acc_29? | Begin_Own_Acc_23? | Begin_Own_Acc_87? | Begin_Own_Acc_63? | Begin_Own_Acc_36? | Begin_Own_Acc_39? | Begin_Own_Acc_14? | Begin_Own_Acc_91? | Begin_Own_Acc_40? | Begin_Own_Acc_15? | Begin_Own_Acc_57? | Begin_Own_Acc_98? | Begin_Own_Acc_38? | Begin_Own_Acc_55? | Begin_Own_Acc_44? | Begin_Own_Acc_90? | Begin_Own_Acc_5? | Begin_Own_Acc_68? | Begin_Own_Acc_10? | Begin_Own_Acc_9? | Begin_Own_Acc_71? | Begin_Own_Acc_77? | Begin_Own_Acc_78? | Begin_Own_Acc_84? | Begin_Own_Acc_11? | Begin_Own_Acc_88? | Begin_Own_Acc_70? | Begin_Own_Acc_50? | Begin_Own_Acc_7? | Begin_Own_Acc_62? | Begin_Own_Acc_85? | Begin_Own_Acc_83? | Begin_Own_Acc_51? | Begin_Own_Acc_41? | Begin_Own_Acc_96? | Begin_Own_Acc_34? | Begin_Own_Acc_19? | Begin_Own_Acc_100? | Begin_Own_Acc_27? | Begin_Own_Acc_53? | Begin_Own_Acc_58? | Begin_Own_Acc_86? | Begin_Own_Acc_35? | Begin_Own_Acc_94? | Begin_Own_Acc_3? | Begin_Own_Acc_97? | Begin_Own_Acc_21? | Begin_Own_Acc_6? | Begin_Own_Acc_17? | Begin_Own_Acc_37? | Begin_Own_Acc_59? | Begin_Own_Acc_28? | Begin_Own_Acc_81? | Begin_Own_Acc_1? | Begin_Own_Acc_47? | Begin_Own_Acc_13? | Begin_Own_Acc_82? | Begin_Own_Acc_31? | Begin_Own_Acc_79? | Begin_Own_Acc_30? | Begin_Own_Acc_99? | Begin_Own_Acc_60? | Begin_Own_Acc_2? | Begin_Own_Acc_74? | Begin_Own_Acc_49? | Begin_Own_Acc_4? | Begin_Own_Acc_93? | Begin_Own_Acc_95? | Begin_Own_Acc_42? | Begin_Own_Acc_54? | Begin_Own_Acc_20? | Begin_Own_Acc_16? | Begin_Own_Acc_65? | Begin_Own_Acc_26? | Begin_Own_Acc_89? | Begin_Own_Acc_45? | Begin_Own_Acc_92? | Begin_Own_Acc_24? | Begin_Own_Acc_32? | Begin_Own_Acc_46? | Begin_Own_Acc_43? | Begin_Own_Acc_69? | Begin_Own_Acc_72? | Begin_Own_Acc_48? | Begin_Own_Acc_8? | Begin_Own_Acc_73? | Begin_Own_Acc_52? | Begin_Own_Acc_76? | Begin_Own_Acc_25? | Begin_Own_Acc_61? | Begin_Own_Acc_67? | Begin_Own_Acc_33? | Begin_Own_Acc_75? | Begin_Own_Acc_18? | Begin_Own_Acc_12? | Begin_Own_Acc_22? | Begin_Own_Acc_80? | Begin_Own_Acc_64? | Begin_Own_Acc_66?) | (Req_Ext_Acc_35? | Req_Ext_Acc_14? | Req_Ext_Acc_79? | Req_Ext_Acc_62? | Req_Ext_Acc_86? | Req_Ext_Acc_97? | Req_Ext_Acc_69? | Req_Ext_Acc_68? | Req_Ext_Acc_84? | Req_Ext_Acc_7? | Req_Ext_Acc_61? | Req_Ext_Acc_66? | Req_Ext_Acc_22? | Req_Ext_Acc_59? | Req_Ext_Acc_51? | Req_Ext_Acc_38? | Req_Ext_Acc_80? | Req_Ext_Acc_17? | Req_Ext_Acc_1? | Req_Ext_Acc_87? | Req_Ext_Acc_37? | Req_Ext_Acc_3? | Req_Ext_Acc_11? | Req_Ext_Acc_33? | Req_Ext_Acc_78? | Req_Ext_Acc_94? | Req_Ext_Acc_5? | Req_Ext_Acc_65? | Req_Ext_Acc_10? | Req_Ext_Acc_20? | Req_Ext_Acc_56? | Req_Ext_Acc_25? | Req_Ext_Acc_48? | Req_Ext_Acc_2? | Req_Ext_Acc_93? | Req_Ext_Acc_34? | Req_Ext_Acc_49? | Req_Ext_Acc_42? | Req_Ext_Acc_54? | Req_Ext_Acc_31? | Req_Ext_Acc_63? | Req_Ext_Acc_64? | Req_Ext_Acc_81? | Req_Ext_Acc_71? | Req_Ext_Acc_50? | Req_Ext_Acc_72? | Req_Ext_Acc_43? | Req_Ext_Acc_32? | Req_Ext_Acc_19? | Req_Ext_Acc_82? | Req_Ext_Acc_83? | Req_Ext_Acc_58? | Req_Ext_Acc_55? | Req_Ext_Acc_96? | Req_Ext_Acc_73? | Req_Ext_Acc_28? | Req_Ext_Acc_27? | Req_Ext_Acc_30? | Req_Ext_Acc_36? | Req_Ext_Acc_60? | Req_Ext_Acc_4? | Req_Ext_Acc_12? | Req_Ext_Acc_29? | Req_Ext_Acc_70? | Req_Ext_Acc_44? | Req_Ext_Acc_9? | Req_Ext_Acc_52? | Req_Ext_Acc_92? | Req_Ext_Acc_88? | Req_Ext_Acc_15? | Req_Ext_Acc_40? | Req_Ext_Acc_74? | Req_Ext_Acc_91? | Req_Ext_Acc_46? | Req_Ext_Acc_24? | Req_Ext_Acc_98? | Req_Ext_Acc_100? | Req_Ext_Acc_90? | Req_Ext_Acc_57? | Req_Ext_Acc_39? | Req_Ext_Acc_53? | Req_Ext_Acc_6? | Req_Ext_Acc_41? | Req_Ext_Acc_76? | Req_Ext_Acc_47? | Req_Ext_Acc_99? | Req_Ext_Acc_21? | Req_Ext_Acc_16? | Req_Ext_Acc_45? | Req_Ext_Acc_8? | Req_Ext_Acc_26? | Req_Ext_Acc_89? | Req_Ext_Acc_77? | Req_Ext_Acc_67? | Req_Ext_Acc_85? | Req_Ext_Acc_75? | Req_Ext_Acc_18? | Req_Ext_Acc_13? | Req_Ext_Acc_23? | Req_Ext_Acc_95?))
ctl p_1883_mix_full_and_notx: E F ((Begin_Own_Acc_56? | Begin_Own_Acc_29? | Begin_Own_Acc_23? | Begin_Own_Acc_87? | Begin_Own_Acc_63? | Begin_Own_Acc_36? | Begin_Own_Acc_39? | Begin_Own_Acc_14? | Begin_Own_Acc_91? | Begin_Own_Acc_40? | Begin_Own_Acc_15? | Begin_Own_Acc_57? | Begin_Own_Acc_98? | Begin_Own_Acc_38? | Begin_Own_Acc_55? | Begin_Own_Acc_44? | Begin_Own_Acc_90? | Begin_Own_Acc_5? | Begin_Own_Acc_68? | Begin_Own_Acc_10? | Begin_Own_Acc_9? | Begin_Own_Acc_71? | Begin_Own_Acc_77? | Begin_Own_Acc_78? | Begin_Own_Acc_84? | Begin_Own_Acc_11? | Begin_Own_Acc_88? | Begin_Own_Acc_70? | Begin_Own_Acc_50? | Begin_Own_Acc_7? | Begin_Own_Acc_62? | Begin_Own_Acc_85? | Begin_Own_Acc_83? | Begin_Own_Acc_51? | Begin_Own_Acc_41? | Begin_Own_Acc_96? | Begin_Own_Acc_34? | Begin_Own_Acc_19? | Begin_Own_Acc_100? | Begin_Own_Acc_27? | Begin_Own_Acc_53? | Begin_Own_Acc_58? | Begin_Own_Acc_86? | Begin_Own_Acc_35? | Begin_Own_Acc_94? | Begin_Own_Acc_3? | Begin_Own_Acc_97? | Begin_Own_Acc_21? | Begin_Own_Acc_6? | Begin_Own_Acc_17? | Begin_Own_Acc_37? | Begin_Own_Acc_59? | Begin_Own_Acc_28? | Begin_Own_Acc_81? | Begin_Own_Acc_1? | Begin_Own_Acc_47? | Begin_Own_Acc_13? | Begin_Own_Acc_82? | Begin_Own_Acc_31? | Begin_Own_Acc_79? | Begin_Own_Acc_30? | Begin_Own_Acc_99? | Begin_Own_Acc_60? | Begin_Own_Acc_2? | Begin_Own_Acc_74? | Begin_Own_Acc_49? | Begin_Own_Acc_4? | Begin_Own_Acc_93? | Begin_Own_Acc_95? | Begin_Own_Acc_42? | Begin_Own_Acc_54? | Begin_Own_Acc_20? | Begin_Own_Acc_16? | Begin_Own_Acc_65? | Begin_Own_Acc_26? | Begin_Own_Acc_89? | Begin_Own_Acc_45? | Begin_Own_Acc_92? | Begin_Own_Acc_24? | Begin_Own_Acc_32? | Begin_Own_Acc_46? | Begin_Own_Acc_43? | Begin_Own_Acc_69? | Begin_Own_Acc_72? | Begin_Own_Acc_48? | Begin_Own_Acc_8? | Begin_Own_Acc_73? | Begin_Own_Acc_52? | Begin_Own_Acc_76? | Begin_Own_Acc_25? | Begin_Own_Acc_61? | Begin_Own_Acc_67? | Begin_Own_Acc_33? | Begin_Own_Acc_75? | Begin_Own_Acc_18? | Begin_Own_Acc_12? | Begin_Own_Acc_22? | Begin_Own_Acc_80? | Begin_Own_Acc_64? | Begin_Own_Acc_66?) & !(Req_Ext_Acc_35? | Req_Ext_Acc_14? | Req_Ext_Acc_79? | Req_Ext_Acc_62? | Req_Ext_Acc_86? | Req_Ext_Acc_97? | Req_Ext_Acc_69? | Req_Ext_Acc_68? | Req_Ext_Acc_84? | Req_Ext_Acc_7? | Req_Ext_Acc_61? | Req_Ext_Acc_66? | Req_Ext_Acc_22? | Req_Ext_Acc_59? | Req_Ext_Acc_51? | Req_Ext_Acc_38? | Req_Ext_Acc_80? | Req_Ext_Acc_17? | Req_Ext_Acc_1? | Req_Ext_Acc_87? | Req_Ext_Acc_37? | Req_Ext_Acc_3? | Req_Ext_Acc_11? | Req_Ext_Acc_33? | Req_Ext_Acc_78? | Req_Ext_Acc_94? | Req_Ext_Acc_5? | Req_Ext_Acc_65? | Req_Ext_Acc_10? | Req_Ext_Acc_20? | Req_Ext_Acc_56? | Req_Ext_Acc_25? | Req_Ext_Acc_48? | Req_Ext_Acc_2? | Req_Ext_Acc_93? | Req_Ext_Acc_34? | Req_Ext_Acc_49? | Req_Ext_Acc_42? | Req_Ext_Acc_54? | Req_Ext_Acc_31? | Req_Ext_Acc_63? | Req_Ext_Acc_64? | Req_Ext_Acc_81? | Req_Ext_Acc_71? | Req_Ext_Acc_50? | Req_Ext_Acc_72? | Req_Ext_Acc_43? | Req_Ext_Acc_32? | Req_Ext_Acc_19? | Req_Ext_Acc_82? | Req_Ext_Acc_83? | Req_Ext_Acc_58? | Req_Ext_Acc_55? | Req_Ext_Acc_96? | Req_Ext_Acc_73? | Req_Ext_Acc_28? | Req_Ext_Acc_27? | Req_Ext_Acc_30? | Req_Ext_Acc_36? | Req_Ext_Acc_60? | Req_Ext_Acc_4? | Req_Ext_Acc_12? | Req_Ext_Acc_29? | Req_Ext_Acc_70? | Req_Ext_Acc_44? | Req_Ext_Acc_9? | Req_Ext_Acc_52? | Req_Ext_Acc_92? | Req_Ext_Acc_88? | Req_Ext_Acc_15? | Req_Ext_Acc_40? | Req_Ext_Acc_74? | Req_Ext_Acc_91? | Req_Ext_Acc_46? | Req_Ext_Acc_24? | Req_Ext_Acc_98? | Req_Ext_Acc_100? | Req_Ext_Acc_90? | Req_Ext_Acc_57? | Req_Ext_Acc_39? | Req_Ext_Acc_53? | Req_Ext_Acc_6? | Req_Ext_Acc_41? | Req_Ext_Acc_76? | Req_Ext_Acc_47? | Req_Ext_Acc_99? | Req_Ext_Acc_21? | Req_Ext_Acc_16? | Req_Ext_Acc_45? | Req_Ext_Acc_8? | Req_Ext_Acc_26? | Req_Ext_Acc_89? | Req_Ext_Acc_77? | Req_Ext_Acc_67? | Req_Ext_Acc_85? | Req_Ext_Acc_75? | Req_Ext_Acc_18? | Req_Ext_Acc_13? | Req_Ext_Acc_23? | Req_Ext_Acc_95?))


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