Commit 859d32e7 authored by Philipp Meyer's avatar Philipp Meyer

Added 1-safe property for SAP benchmarks

parent 0eb8cb83

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.
EF ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((FALSE OR i >= 2) OR o >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___InputCondition >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Split_Split_and__10qo_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Split_Join_and__10qo_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Join_Split_Product_description_using_Configuration_Management__10tm_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Join_Join_Product_description_using_Configuration_Management__10tm_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___outputCondition >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Split_Yes_and__10qo__and__10qo_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Document_Structure_Processing__10p7_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Material_Master_Processing__10pz_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Characteristic_Processing__10r2_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Edit_Classes__10ry_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Classification__10su_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Material_BOM_Processing__10yv_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__Document_Processing__110o_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Document_Structure_Processing__10p7__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10ya__and__10z2_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__Configuration_Profile_Processing__10u0_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__Object_Dependency_Maintenance__10us_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__Variant_Table_Processing__10vs_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__Variant_Function_Processing__10x3_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__Variant_Condition_Processing__10y3_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__Material_Variant_Processing__1112_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Configuration_Profile_Processing__10u0__and__10yh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10yh__Configuration_Simulation__10qh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Configuration_Simulation__10qh__and__10t1_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10t1__Routing_Processing__10zi_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10t1__Inspection_Plan_Processing__10zw_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Routing_Processing__10zi__and__10t8_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10t8__Production_Resource__Tool_Processing__10pl_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Production_Resource__Tool_Processing__10pl__Order_BOM_Processing__10ri_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Order_BOM_Processing__10ri__and__10u7_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10u7__Graphical_Product_Structure_Processing__10sg_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10u7__Integrated_Product_and_Process_Data_Processing___EWB__110a_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Graphical_Product_Structure_Processing__10sg__and__10ue_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10ue__Product_description_using_Configuration_Management__10tm_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Product_description_using_Configuration_Management__10tm__Join_Yes_Product_description_using_Configuration_Management__10tm_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Material_Master_Processing__10pz__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Characteristic_Processing__10r2__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Edit_Classes__10ry__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Classification__10su__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Material_BOM_Processing__10yv__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Document_Processing__110o__and__10ya_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Object_Dependency_Maintenance__10us__and__10yh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Variant_Table_Processing__10vs__and__10yh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Variant_Function_Processing__10x3__and__10yh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Variant_Condition_Processing__10y3__and__10yh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Material_Variant_Processing__1112__and__10yh_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Inspection_Plan_Processing__10zw__and__10t8_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Integrated_Product_and_Process_Data_Processing___EWB__110a__and__10ue_ >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Split_busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Split_No_and__10qo__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Split_Yes_and__10qo__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Skip_busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10qo__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Document_Structure_Processing__10p7__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10ya__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10z2__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Configuration_Profile_Processing__10u0__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10yh__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Configuration_Simulation__10qh__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10t1__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Routing_Processing__10zi__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10t8__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Production_Resource__Tool_Processing__10pl__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Order_BOM_Processing__10ri__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10u7__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Graphical_Product_Structure_Processing__10sg__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___and__10ue__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Product_description_using_Configuration_Management__10tm__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Material_Master_Processing__10pz__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Characteristic_Processing__10r2__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Edit_Classes__10ry__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Classification__10su__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Material_BOM_Processing__10yv__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Document_Processing__110o__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Object_Dependency_Maintenance__10us__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Variant_Table_Processing__10vs__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Variant_Function_Processing__10x3__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Variant_Condition_Processing__10y3__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Material_Variant_Processing__1112__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Inspection_Plan_Processing__10zw__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Integrated_Product_and_Process_Data_Processing___EWB__110a__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Join_No_Product_description_using_Configuration_Management__10tm__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Join_Yes_Product_description_using_Configuration_Management__10tm__busy >= 2) OR p_Model_10om__0_____u___Model_10om__0_____u___Output_busy >= 2))
PLACE i,o,p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_,p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_,p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_,p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy,p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy;
MARKING i:1;
TRANSITION __Model_18wm__0_____u___Model_18wm__0_____u___start
CONSUME i:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition:1;
TRANSITION __Model_18wm__0_____u___Model_18wm__0_____u___end
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___outputCondition:1;
PRODUCE o:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_join_InputCondition
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___InputCondition:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_split_Split_Split_and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__join_Split_Split_and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__split_Split_Join_and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_No_and__18yh__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__join_Split_Split_and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Split_and__18yh_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__split_Split_Join_and__18yh__Split_Yes_and__18yh__and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Skip_join_Split_Join_and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Join_and__18yh_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Skip_split_Join_Split_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Skip_busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__join_Split_Yes_and__18yh__and__18yh_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Split_Yes_and__18yh__and__18yh_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__split_and__18yh__Find_Object__18xe__and__18yh__Material_Search__18xs__and__18yh__Document_Search__18y6_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__join_and__18yh__Find_Object__18xe_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Find_Object__18xe_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__split_Find_Object__18xe__and__18ys_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__join_Find_Object__18xe__and__18ys__Material_Search__18xs__and__18ys__Document_Search__18y6__and__18ys_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Find_Object__18xe__and__18ys_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__split_and__18ys__xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__join_and__18ys__xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18ys__xor__18x0_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__split_xor__18x0__Join_Yes_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__join_and__18yh__Material_Search__18xs_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Material_Search__18xs_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__split_Material_Search__18xs__and__18ys_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Material_Search__18xs__and__18ys_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__join_and__18yh__Document_Search__18y6_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___and__18yh__Document_Search__18y6_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__split_Document_Search__18y6__and__18ys_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Document_Search__18y6__and__18ys_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__join_Join_Split_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__split_Join_Join_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Join_No_xor__18x0__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__join_xor__18x0__Join_Yes_xor__18x0__Join_Split_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___xor__18x0__Join_Yes_xor__18x0_:1,p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Split_xor__18x0_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__split_Join_Join_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Yes_xor__18x0__busy:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_:1;
TRANSITION t_Model_18wm__0_____u___Model_18wm__0_____u___Output_join_Join_Join_xor__18x0_
CONSUME p_Model_18wm__0_____u___Model_18wm__0_____u___Join_Join_xor__18x0_:1;
PRODUCE p_Model_18wm__0_____u___Model_18wm__0_____u___Output_busy:1;