diff --git a/.gitignore b/.gitignore index 9491a2f..8e5795e 100644 --- a/.gitignore +++ b/.gitignore @@ -360,4 +360,5 @@ MigrationBackup/ .ionide/ # Fody - auto-generated XML schema -FodyWeavers.xsd \ No newline at end of file +FodyWeavers.xsd +/.idea/.idea.DataPetriNet/.idea diff --git a/DataPetriNet.sln b/DataPetriNet.sln index e292417..2f05cfd 100644 --- a/DataPetriNet.sln +++ b/DataPetriNet.sln @@ -23,74 +23,108 @@ Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU Debug|x64 = Debug|x64 + Debug|x86 = Debug|x86 Release|Any CPU = Release|Any CPU Release|x64 = Release|x64 + Release|x86 = Release|x86 EndGlobalSection GlobalSection(ProjectConfigurationPlatforms) = postSolution {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Debug|Any CPU.Build.0 = Debug|Any CPU {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Debug|x64.ActiveCfg = Debug|x64 {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Debug|x64.Build.0 = Debug|x64 + {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Debug|x86.ActiveCfg = Debug|Any CPU + {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Debug|x86.Build.0 = Debug|Any CPU {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Release|Any CPU.ActiveCfg = Release|Any CPU {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Release|Any CPU.Build.0 = Release|Any CPU {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Release|x64.ActiveCfg = Release|x64 {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Release|x64.Build.0 = Release|x64 + {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Release|x86.ActiveCfg = Release|Any CPU + {F76B2DA4-35E8-4127-9350-87F7A6C938BE}.Release|x86.Build.0 = Release|Any CPU {CCA5638A-4561-4CCB-9904-7A5163681538}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {CCA5638A-4561-4CCB-9904-7A5163681538}.Debug|Any CPU.Build.0 = Debug|Any CPU {CCA5638A-4561-4CCB-9904-7A5163681538}.Debug|x64.ActiveCfg = Debug|x64 {CCA5638A-4561-4CCB-9904-7A5163681538}.Debug|x64.Build.0 = Debug|x64 + {CCA5638A-4561-4CCB-9904-7A5163681538}.Debug|x86.ActiveCfg = Debug|Any CPU + {CCA5638A-4561-4CCB-9904-7A5163681538}.Debug|x86.Build.0 = Debug|Any CPU {CCA5638A-4561-4CCB-9904-7A5163681538}.Release|Any CPU.ActiveCfg = Release|Any CPU {CCA5638A-4561-4CCB-9904-7A5163681538}.Release|Any CPU.Build.0 = Release|Any CPU {CCA5638A-4561-4CCB-9904-7A5163681538}.Release|x64.ActiveCfg = Release|x64 {CCA5638A-4561-4CCB-9904-7A5163681538}.Release|x64.Build.0 = Release|x64 + {CCA5638A-4561-4CCB-9904-7A5163681538}.Release|x86.ActiveCfg = Release|Any CPU + {CCA5638A-4561-4CCB-9904-7A5163681538}.Release|x86.Build.0 = Release|Any CPU {675C092D-7139-47D6-AA77-3AEE7B263100}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {675C092D-7139-47D6-AA77-3AEE7B263100}.Debug|Any CPU.Build.0 = Debug|Any CPU {675C092D-7139-47D6-AA77-3AEE7B263100}.Debug|x64.ActiveCfg = Debug|x64 {675C092D-7139-47D6-AA77-3AEE7B263100}.Debug|x64.Build.0 = Debug|x64 + {675C092D-7139-47D6-AA77-3AEE7B263100}.Debug|x86.ActiveCfg = Debug|Any CPU + {675C092D-7139-47D6-AA77-3AEE7B263100}.Debug|x86.Build.0 = Debug|Any CPU {675C092D-7139-47D6-AA77-3AEE7B263100}.Release|Any CPU.ActiveCfg = Release|Any CPU {675C092D-7139-47D6-AA77-3AEE7B263100}.Release|Any CPU.Build.0 = Release|Any CPU {675C092D-7139-47D6-AA77-3AEE7B263100}.Release|x64.ActiveCfg = Release|x64 {675C092D-7139-47D6-AA77-3AEE7B263100}.Release|x64.Build.0 = Release|x64 + {675C092D-7139-47D6-AA77-3AEE7B263100}.Release|x86.ActiveCfg = Release|Any CPU + {675C092D-7139-47D6-AA77-3AEE7B263100}.Release|x86.Build.0 = Release|Any CPU {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Debug|Any CPU.Build.0 = Debug|Any CPU {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Debug|x64.ActiveCfg = Debug|x64 {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Debug|x64.Build.0 = Debug|x64 + {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Debug|x86.ActiveCfg = Debug|x86 + {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Debug|x86.Build.0 = Debug|x86 {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Release|Any CPU.ActiveCfg = Release|Any CPU {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Release|Any CPU.Build.0 = Release|Any CPU {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Release|x64.ActiveCfg = Release|x64 {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Release|x64.Build.0 = Release|x64 + {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Release|x86.ActiveCfg = Release|x86 + {747EEDAD-7C8E-4AB2-9D16-0BF7FF664395}.Release|x86.Build.0 = Release|x86 {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|Any CPU.Build.0 = Debug|Any CPU - {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|x64.ActiveCfg = Debug|Any CPU - {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|x64.Build.0 = Debug|Any CPU + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|x64.ActiveCfg = Debug|x64 + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|x64.Build.0 = Debug|x64 + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|x86.ActiveCfg = Debug|x86 + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Debug|x86.Build.0 = Debug|x86 {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|Any CPU.ActiveCfg = Release|Any CPU {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|Any CPU.Build.0 = Release|Any CPU - {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|x64.ActiveCfg = Release|Any CPU - {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|x64.Build.0 = Release|Any CPU + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|x64.ActiveCfg = Release|x64 + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|x64.Build.0 = Release|x64 + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|x86.ActiveCfg = Release|x86 + {F1A65E68-B269-4CD6-B1E5-A7513F6847DE}.Release|x86.Build.0 = Release|x86 {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Debug|Any CPU.Build.0 = Debug|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Debug|x64.ActiveCfg = Debug|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Debug|x64.Build.0 = Debug|Any CPU + {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Debug|x86.ActiveCfg = Debug|Any CPU + {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Debug|x86.Build.0 = Debug|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Release|Any CPU.ActiveCfg = Release|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Release|Any CPU.Build.0 = Release|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Release|x64.ActiveCfg = Release|Any CPU {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Release|x64.Build.0 = Release|Any CPU + {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Release|x86.ActiveCfg = Release|Any CPU + {3405D568-157D-47B7-B592-F3D59AE1EB6A}.Release|x86.Build.0 = Release|Any CPU {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|Any CPU.Build.0 = Debug|Any CPU - {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|x64.ActiveCfg = Debug|Any CPU - {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|x64.Build.0 = Debug|Any CPU + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|x64.ActiveCfg = Debug|x64 + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|x64.Build.0 = Debug|x64 + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|x86.ActiveCfg = Debug|Any CPU + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Debug|x86.Build.0 = Debug|Any CPU {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|Any CPU.ActiveCfg = Release|Any CPU {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|Any CPU.Build.0 = Release|Any CPU - {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|x64.ActiveCfg = Release|Any CPU - {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|x64.Build.0 = Release|Any CPU + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|x64.ActiveCfg = Release|x64 + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|x64.Build.0 = Release|x64 + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|x86.ActiveCfg = Release|Any CPU + {5C7B2000-3119-4A16-811D-433FAED64C0A}.Release|x86.Build.0 = Release|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Debug|Any CPU.Build.0 = Debug|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Debug|x64.ActiveCfg = Debug|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Debug|x64.Build.0 = Debug|Any CPU + {428C3071-124C-4A23-B986-D2ABFEE257BC}.Debug|x86.ActiveCfg = Debug|Any CPU + {428C3071-124C-4A23-B986-D2ABFEE257BC}.Debug|x86.Build.0 = Debug|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Release|Any CPU.ActiveCfg = Release|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Release|Any CPU.Build.0 = Release|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Release|x64.ActiveCfg = Release|Any CPU {428C3071-124C-4A23-B986-D2ABFEE257BC}.Release|x64.Build.0 = Release|Any CPU + {428C3071-124C-4A23-B986-D2ABFEE257BC}.Release|x86.ActiveCfg = Release|Any CPU + {428C3071-124C-4A23-B986-D2ABFEE257BC}.Release|x86.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/DataPetriNetGeneration/DataPetriNetGeneration.csproj b/DataPetriNetGeneration/DataPetriNetGeneration.csproj index cad45b3..1b56c32 100644 --- a/DataPetriNetGeneration/DataPetriNetGeneration.csproj +++ b/DataPetriNetGeneration/DataPetriNetGeneration.csproj @@ -7,6 +7,10 @@ AnyCPU;x86;x64 + + + + diff --git a/DataPetriNetIterativeVerificationApplication/Configuration.json b/DataPetriNetIterativeVerificationApplication/Configuration.json index 17d6b69..dc676e1 100644 --- a/DataPetriNetIterativeVerificationApplication/Configuration.json +++ b/DataPetriNetIterativeVerificationApplication/Configuration.json @@ -1,4 +1,4 @@ { - "DPNVerificationApplicationPath": "C:\\Users\\Admin\\source\\repos\\DataPetriNet\\DataPetriNetVerificationApplication\\bin\\Debug\\net6.0\\DataPetriNetVerificationApplication.exe", - "DPNVerificationApplicationWorkingDir": "C:\\Users\\Admin\\source\\repos\\DataPetriNet\\DataPetriNetVerificationApplication\\bin\\Debug\\net6.0\\" + "DPNVerificationApplicationPath": "C:\\Users\\Admin\\source\\repos\\DataPetriNet\\DataPetriNetVerificationApplication\\bin\\x64\\Release\\net6.0\\DataPetriNetVerificationApplication.exe", + "DPNVerificationApplicationWorkingDir": "C:\\Users\\Admin\\source\\repos\\DataPetriNet\\DataPetriNetVerificationApplication\\bin\\x64\\Release\\net6.0\\" } diff --git a/DataPetriNetIterativeVerificationApplication/DataPetriNetIterativeVerificationApplication.csproj b/DataPetriNetIterativeVerificationApplication/DataPetriNetIterativeVerificationApplication.csproj index d7ee66f..d304893 100644 --- a/DataPetriNetIterativeVerificationApplication/DataPetriNetIterativeVerificationApplication.csproj +++ b/DataPetriNetIterativeVerificationApplication/DataPetriNetIterativeVerificationApplication.csproj @@ -5,6 +5,7 @@ net6.0-windows enable true + AnyCPU;x86;x64 @@ -17,6 +18,7 @@ + @@ -34,7 +36,7 @@ - PreserveNewest + Always diff --git a/DataPetriNetIterativeVerificationApplication/MainWindow.xaml.cs b/DataPetriNetIterativeVerificationApplication/MainWindow.xaml.cs index 965a003..333b54d 100644 --- a/DataPetriNetIterativeVerificationApplication/MainWindow.xaml.cs +++ b/DataPetriNetIterativeVerificationApplication/MainWindow.xaml.cs @@ -40,7 +40,7 @@ public partial class MainWindow : Window private Dictionary paths = new Dictionary(); private ObservableCollection verificationResults = new(); private CancellationTokenSource source; - private VerificationRunner verificationRunner = new(); + private VerificationRunner verificationRunner; public MainWindow() { InitializeComponent(); @@ -75,6 +75,8 @@ public MainWindow() MaxConditionsTb.Text = "150"; MaxVarsTb.Text = "150"; + verificationRunner = new(); + VerificationDG.ItemsSource = verificationResults; verificationResults.CollectionChanged += listChanged; } diff --git a/DataPetriNetIterativeVerificationApplication/Services/IterativeVerificationRunner.cs b/DataPetriNetIterativeVerificationApplication/Services/IterativeVerificationRunner.cs index db50671..3d46f65 100644 --- a/DataPetriNetIterativeVerificationApplication/Services/IterativeVerificationRunner.cs +++ b/DataPetriNetIterativeVerificationApplication/Services/IterativeVerificationRunner.cs @@ -149,7 +149,7 @@ public async Task RunIterativeVerificationLoop( var verificationTypes = new List { VerificationAlgorithmTypeEnum.ImprovedVersion, - VerificationAlgorithmTypeEnum.DirectVersion + //VerificationAlgorithmTypeEnum.DirectVersion }; do @@ -162,11 +162,11 @@ public async Task RunIterativeVerificationLoop( var soundnessPreference = verificationInput.ConditionsInfo.Soundness.GetValueOrDefault(); var dpn = dpnGenerator.Generate( - (int)(verificationInput.DpnInfo.Places * n), - (int)(verificationInput.DpnInfo.Transitions * n), - (int)(verificationInput.DpnInfo.ExtraArcs * n), - (int)(verificationInput.DpnInfo.Variables * n), - (int)(verificationInput.DpnInfo.Conditions * n), + (int)Math.Round(verificationInput.DpnInfo.Places * n), + (int)Math.Round(verificationInput.DpnInfo.Transitions * n), + (int)Math.Round(verificationInput.DpnInfo.ExtraArcs * n), + (int)Math.Round(verificationInput.DpnInfo.Variables * n), + (int)Math.Round(verificationInput.DpnInfo.Conditions * n), soundnessPreference); dpn.Name = Guid.NewGuid().ToString(); diff --git a/DataPetriNetOnSmt.Tests/DataPetriNetOnSmt.Tests.csproj b/DataPetriNetOnSmt.Tests/DataPetriNetOnSmt.Tests.csproj index a98da64..123b334 100644 --- a/DataPetriNetOnSmt.Tests/DataPetriNetOnSmt.Tests.csproj +++ b/DataPetriNetOnSmt.Tests/DataPetriNetOnSmt.Tests.csproj @@ -11,6 +11,7 @@ + diff --git a/DataPetriNetOnSmt.Visualization/DataPetriNetOnSmt.Visualization.csproj b/DataPetriNetOnSmt.Visualization/DataPetriNetOnSmt.Visualization.csproj index 58b7d2b..719c00e 100644 --- a/DataPetriNetOnSmt.Visualization/DataPetriNetOnSmt.Visualization.csproj +++ b/DataPetriNetOnSmt.Visualization/DataPetriNetOnSmt.Visualization.csproj @@ -13,6 +13,7 @@ + diff --git a/DataPetriNetOnSmt.Visualization/MainWindow.xaml.cs b/DataPetriNetOnSmt.Visualization/MainWindow.xaml.cs index dd9c472..6bbd7c3 100644 --- a/DataPetriNetOnSmt.Visualization/MainWindow.xaml.cs +++ b/DataPetriNetOnSmt.Visualization/MainWindow.xaml.cs @@ -207,7 +207,7 @@ private void TransformModelToAtomicItem_Click(object sender, RoutedEventArgs e) } private void TransformModelToRefinedItem_Click(object sender, RoutedEventArgs e) - { + { var dpnTransformation = new TransformerToRefined(); /*var stopWatch = new Stopwatch(); @@ -265,11 +265,11 @@ private void TransformModelToRepairedItem_Click(object sender, RoutedEventArgs e var stopwatch = new Stopwatch(); stopwatch.Start(); - (currentDisplayedNet, var result) = dpnRepairment.RepairDpn(currentDisplayedNet); + (currentDisplayedNet, var repairSteps, var result) = dpnRepairment.RepairDpn(currentDisplayedNet); stopwatch.Stop(); - MessageBox.Show(result ? $"Success! Time spent: {stopwatch.ElapsedMilliseconds}ms" : "Failure!"); + MessageBox.Show(result ? $"Success! Time spent: {stopwatch.ElapsedMilliseconds} ms. Repair steps: {repairSteps}." : "Failure!"); graphControl.Graph = dpnParser.FormGraphBasedOnDPN(currentDisplayedNet); } } diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/DigitalWhiteboard_Discharge.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/DigitalWhiteboard_Discharge.pnmlx new file mode 100644 index 0000000..43a27e9 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/DigitalWhiteboard_Discharge.pnmlx @@ -0,0 +1,150 @@ + + + + + Digital whiteboard: discharge + + + + + start + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + end + + + 1 + + + + + bed status + + + + + bed status + + + + + move to history + + + + + move to history + + + + + Transfer + + + + + Transfer + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + + org1 + + + org2 + + + statusLedig + + + valueHistory + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/DigitalWhiteboard_Transfer.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/DigitalWhiteboard_Transfer.pnmlx new file mode 100644 index 0000000..054b08f --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/DigitalWhiteboard_Transfer.pnmlx @@ -0,0 +1,152 @@ + + + + + Digital whiteboard: transfer + + + + + start + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + end + + + 1 + + + + + bed status + + + + + bed status + + + + + Eom + + + + + Eom + + + + + Transfer + + + + + Transfer + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + + org1 + + + org2 + + + roomTransfer + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/BpmnExample.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/BpmnExample.pnmlx new file mode 100644 index 0000000..748d18d --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/BpmnExample.pnmlx @@ -0,0 +1,250 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + p8 + + + + + o + + + 1 + + + + + Loan Request + + + + + AndS + + + + + Repayment Computation + + + + + History Evaluation + + + + + AndJ + + + + + Early Rejection + + + + + Preliminary Approval + + + + + Detailed Investigation + + + + + Rejection + + + + + + Loan Issue + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + amount + + + age + + + salary + + + repayment + + + goodhistory + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Counterexample.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Counterexample.pnmlx new file mode 100644 index 0000000..85a266f --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Counterexample.pnmlx @@ -0,0 +1,271 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + p8 + + + + + o + + + 1 + + + + + t1 + + + + + t2 + + + + + t3 + + + + + t4 + + + + + t5 + + + + + t6 + + + + + t7 + + + + + t8 + + + + + t9 + + + + + + t10 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + + a + + + b + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/DigitalWhiteboard_Transfer.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/DigitalWhiteboard_Transfer.pnmlx new file mode 100644 index 0000000..9ef1429 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/DigitalWhiteboard_Transfer.pnmlx @@ -0,0 +1,152 @@ + + + + + Digital whiteboard: transfer + + + + + start + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + end + + + 1 + + + + + bed status 1 + + + + + bed status 2 + + + + + Eom 1 + + + + + Eom 2 + + + + + Transfer 1 + + + + + Transfer 2 + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + + org1 + + + org2 + + + roomTransfer + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/For Ada/BpmnExample.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/For Ada/BpmnExample.pnmlx new file mode 100644 index 0000000..93330d0 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/For Ada/BpmnExample.pnmlx @@ -0,0 +1,250 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + p8 + + + + + o + + + 1 + + + + + Loan Request + + + + + AndS + + + + + Repayment Computation + + + + + History Evaluation + + + + + AndJ + + + + + Early Rejection + + + + + Preliminary Approval + + + + + Detailed Investigation + + + + + Rejection + + + + + + Loan Issue + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + amount + + + age + + + salary + + + repayment + + + goodhistory + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/For Ada/Counterexample.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/For Ada/Counterexample.pnmlx new file mode 100644 index 0000000..62f5b8f --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/For Ada/Counterexample.pnmlx @@ -0,0 +1,271 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + p8 + + + + + o + + + 1 + + + + + t1 + + + + + t2 + + + + + t3 + + + + + t4 + + + + + t5 + + + + + t6 + + + + + t7 + + + + + t8 + + + + + t9 + + + + + + t10 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + + a + + + b + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Livelock.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Livelock.pnmlx new file mode 100644 index 0000000..75430ee --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Livelock.pnmlx @@ -0,0 +1,89 @@ + + + + + Boundness check + + + + + i + + + 1 + + + + + + p0 + + + + + + o + + + 1 + + + + + + t0 + + + + + t1 + + + + + t2 + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + a + + + b + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/PackageHandling.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/PackageHandling.pnmlx new file mode 100644 index 0000000..5d12835 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/PackageHandling.pnmlx @@ -0,0 +1,421 @@ + + + + + Package handling + + + + + p0 + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + p8 + + + + + p9 + + + + + p10 + + + + + p11 + + + + + p12 + + + + + p13 + + + + + p14 + + + + + end + + + 1 + + + + + tau1 + + + + + getlength1 + + + + + getlength2 + + + + + getlength3 + + + + + getlengthnoRow + + + + + tau2 + + + + + tau3 + + + + + measure weight + + + + + tau4 + + + + + tau5 + + + + + determinemode1 + + + + + determinemode2 + + + + + determinemode3 + + + + + determinemodenoRow + + + + + tau6 + + + + + tau7 + + + + + chooseconsent1 + + + + + chooseconsent2 + + + + + chooseconsentnoRow + + + + + tau8 + + + + + tau9 + + + + + tau10 + + + + + sign declaration + + + + + tau13 + + + + + tau11 + + + + + fetch + + + + + tau12 + + + + + tau14 + + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + normal + + + + + pL + + + pW + + + pT + + + sM + + + c + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/RoadFines.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/RoadFines.pnmlx new file mode 100644 index 0000000..1a5a9eb --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/RoadFines.pnmlx @@ -0,0 +1,722 @@ + + + + + Road-Fine Management (decision mining) + + + + + pl1 + + + + + + + 1 + + + + + pl6 + + + + + + + + + pl7 + + + + + + + + + end + + + + + + + 1 + + + + + pl10 + + + + + + + + + pl13 + + + + + + + + + pl14 + + + + + + + + + pl15 + + + + + + + + + pl12 + + + + + + + + + Create Fine + + + + + + + + + + Send Fine + + + + + + + + + + Insert Fine Notification + + + + + + + + + + Insert Date Appeal to Prefecture + + + + + + + + + + Inv3 + + + + + + + + + + Inv5 + + + + + + + + + + Inv4 + + + + + + + + + + Appeal to Judge + + + + + + + + + + Send for Credit Collection + + + + + + + + + + Inv1 + + + + + + + + + + Send Appeal to Prefecture + + + + + + + + + + Receive Result Appeal from Prefecture + + + + + + + + + + Notify Result Appeal to Offender + + + + + + + + + + Payment + + + + + + + + + + Add penalty + + + + + + + + + + Inv2 + + + + + + + + + + Payment + + + + + + + + + + Payment + + + + + + + + + + Inv6 + + + + + + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + + amount + + + delayJudge + + + delayPrefecture + + + totalPaymentAmount + + + points + + + dismissal + + + delaySend + + + expenses + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/SimpleAuction.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/SimpleAuction.pnmlx new file mode 100644 index 0000000..c6aacce --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/SimpleAuction.pnmlx @@ -0,0 +1,114 @@ + + + + + simple auction + + + + + start + + + 1 + + + + + p1 + + + + + p2 + + + + + end + + + 1 + + + + + init + + + + + bid + + + + + dec + + + + + expire + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + normal + + + + + + o + + + t + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Unbounded.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Unbounded.pnmlx new file mode 100644 index 0000000..a71a19a --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/For Repair/Unbounded.pnmlx @@ -0,0 +1,125 @@ + + + + + Boundness check + + + + + i + + + 1 + + + + + + p1 + + + + + p2 + + + + + p3 + + + + + + o + + + 1 + + + + + + t1 + + + + + t2 + + + + + t3 + + + + + t4 + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + a + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/HospitalBilling.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/HospitalBilling.pnmlx new file mode 100644 index 0000000..898c624 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/HospitalBilling.pnmlx @@ -0,0 +1,1308 @@ + + + + + Hospital billing + + + + + + + + p1 + + + + + + + + + + p10 + + + + + + + + + + p11 + + + + + + + + + + p12 + + + + + + + + + + p15 + + + + + + + + + + p18 + + + + + + + + + + p2 + + + + + + + + + + p25 + + + + + + + + + + p26 + + + + + + + + + + p27 + + + + + + + + + + p28 + + + + + + + + + + p3 + + + + + + + + + + p40 + + + + + + + + + + p42 + + + + + + + + + + p5 + + + + + + + + + + src + + + + + + + + 1 + + + + + p16 + + + + + + + + 1 + + + + + t1 + + + + + + + + + + CHANGE DIAGN + + + + + + + + + + + t4 + + + + + + + + + + STORNO_1 + + + + + + + + + + + t31 + + + + + + + + + + STORNO_2 + + + + + + + + + + + BILLED1 + + + + + + + + + + + REOPEN1 + + + + + + + + + + + t9 + + + + + + + + + + tLoop + + + + + + + + + + t18 + + + + + + + + + + DELETE2 + + + + + + + + + + + EMPTY + + + + + + + + + + + t7 + + + + + + + + + + t29 + + + + + + + + + + t10 + + + + + + + + + + CHANGE END + + + + + + + + + + + t25 + + + + + + + + + + REJECT + + + + + + + + + + + t39 + + + + + + + + + + BILLED2 + + + + + + + + + + + REOPEN2 + + + + + + + + + + + t15 + + + + + + + + + + SET STATUS + + + + + + + + + + + t30 + + + + + + + + + + DELETE3 + + + + + + + + + + + RELEASE + + + + + + + + + + + REOPEN3 + + + + + + + + + + + skipRelease + + + + + + + + + + FIN + + + + + + + + + + + DELETE1 + + + + + + + + + + + t12 + + + + + + + + + + CODE OK + + + + + + + + + + + t8 + + + + + + + + + + CODE NOK + + + + + + + + + + + NEW + + + + + + + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + normal + + + + + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + + + + + + + + + caseType + + + closeCode + + + speciality + + + isClosed + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/MainCounterExampleToCGMethodWithoutVarDependence.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/MainCounterExampleToCGMethodWithoutVarDependence.pnmlx new file mode 100644 index 0000000..75430ee --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/MainCounterExampleToCGMethodWithoutVarDependence.pnmlx @@ -0,0 +1,89 @@ + + + + + Boundness check + + + + + i + + + 1 + + + + + + p0 + + + + + + o + + + 1 + + + + + + t0 + + + + + t1 + + + + + t2 + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + a + + + b + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/RoadFines.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/RoadFines.pnmlx new file mode 100644 index 0000000..1a5a9eb --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/RoadFines.pnmlx @@ -0,0 +1,722 @@ + + + + + Road-Fine Management (decision mining) + + + + + pl1 + + + + + + + 1 + + + + + pl6 + + + + + + + + + pl7 + + + + + + + + + end + + + + + + + 1 + + + + + pl10 + + + + + + + + + pl13 + + + + + + + + + pl14 + + + + + + + + + pl15 + + + + + + + + + pl12 + + + + + + + + + Create Fine + + + + + + + + + + Send Fine + + + + + + + + + + Insert Fine Notification + + + + + + + + + + Insert Date Appeal to Prefecture + + + + + + + + + + Inv3 + + + + + + + + + + Inv5 + + + + + + + + + + Inv4 + + + + + + + + + + Appeal to Judge + + + + + + + + + + Send for Credit Collection + + + + + + + + + + Inv1 + + + + + + + + + + Send Appeal to Prefecture + + + + + + + + + + Receive Result Appeal from Prefecture + + + + + + + + + + Notify Result Appeal to Offender + + + + + + + + + + Payment + + + + + + + + + + Add penalty + + + + + + + + + + Inv2 + + + + + + + + + + Payment + + + + + + + + + + Payment + + + + + + + + + + Inv6 + + + + + + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + + + + + normal + + + + + 1 + + + + + + + + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + normal + + + + + 1 + + + + + + + + + + + + + + normal + + + + + 1 + + + normal + + + + + + amount + + + delayJudge + + + delayPrefecture + + + totalPaymentAmount + + + points + + + dismissal + + + delaySend + + + expenses + + + + diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/RoadFinesNormative.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/RoadFinesNormative.pnmlx new file mode 100644 index 0000000..e69de29 diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/SepsisMined.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/SepsisMined.pnmlx new file mode 100644 index 0000000..1b4eea0 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/SepsisMined.pnmlx @@ -0,0 +1,1529 @@ + + + + + Sepsis mined + + + Mannhardt, F.: Multi-perspective Process Mining. Ph.D. thesis, Technical University of Eindhoven (2018), Fig. 13.6 + + + + + + + + p100 + + + + + + + + + + p101 + + + + + + + + + + p13 + + + + + + + + + + p19 + + + + + + + + + + p2 + + + + + + + + + + end + + + + + + + + + + p22 + + + + + + + + + + p24 + + + + + + + + + + p3 + + + + + + + + + + p31 + + + + + + + + + + p32 + + + + + + + + + + p33 + + + + + + + + + + p34 + + + + + + + + + + p35 + + + + + + + + + + p37 + + + + + + + + + + p38 + + + + + + + + + + p4 + + + + + + + + + + p5 + + + + + + + + + + p700 + + + + + + + + + + p702 + + + + + + + + + + p800 + + + + + + + + + + p802 + + + + + + + + + + source + + + + + + + + 1 + + + + + sink + + + + + + + + 1 + + + + + LacticAcid + + + + + + + + + + + t100 + + + + + + + + + + t25 + + + + + t5 + + + + + + + + + + t6 + + + + + + + + + + ER Sepsis Triage + + + + + + + + + + + t2 + + + + + + + + + + Transfer NC + + + + + + + + + + + ER Triage + + + + + + + + + + + Inv1 + + + + + + + + + + LacticAcid + + + + + + + + + + + AdmissionIC + + + + + + + + + + + Release C + + + + + + + + + + + Release B + + + + + + + + + + + t22 + + + + + + + + + + Release E + + + + + + + + + + + Release D + + + + + + + + + + + Release A + + + + + + + + + + + t800 + + + + + + + + + + Leucocytes + + + + + + + + + + + t38 + + + + + + + + + + Return ER + + + + + + + + + + + IV Liquid + + + + + + + + + + + IV Antibiotics + + + + + + + + + + + t9 + + + + + + + + + + t700 + + + + + + + + + + CRP + + + + + + + + + + + Admission NC + + + + + + + + + + + Admission NC + + + + + + + + + + + Admission IC + + + + + + + + + + + t12 + + + + + + + + + + t703 + + + + + + + + + + CRP + + + + + + + + + + + Leucocytes + + + + + + + + + + + t803 + + + + + + + + + + ER Registration + + + + + + + + + + + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + 1 + + + + normal + + + + + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + 0 + + + + + + + hypotensie + + + diagnosticLacticAcid + + + sirsCriteriaTwo + + + lacticAcid + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-1.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-1.pnmlx new file mode 100644 index 0000000..d2962ee --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-1.pnmlx @@ -0,0 +1,217 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + o + + + 1 + + + + + Loan Request + + + + + Application Review + + + + + Application Rejection + + + + + Repayment Computation + + + + + Request Acceptance + + + + + Request Rejection + + + + + Client Notification + + + + + Documents Preparation + + + + + Loan Issue + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 2 + + + + + 1 + + + + + + + amount + + + age + + + salary + + + repayment + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-2.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-2.pnmlx new file mode 100644 index 0000000..24691e3 --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-2.pnmlx @@ -0,0 +1,230 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + o + + + 1 + + + + + Loan Request + + + + + AndS + + + + + Repayment Computation + + + + + History Evaluation + + + + + AndJ + + + + + Early Rejection + + + + + Detailed Investigation + + + + + Rejection + + + + + + Loan Issue + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + amount + + + age + + + salary + + + repayment + + + goodhistory + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-3.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-3.pnmlx new file mode 100644 index 0000000..c41d4ca --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-3.pnmlx @@ -0,0 +1,230 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + o + + + 1 + + + + + Loan Request + + + + + AndS + + + + + Repayment Computation + + + + + History Evaluation + + + + + AndJ + + + + + Early Rejection + + + + + Detailed Investigation + + + + + Rejection + + + + + + Loan Issue + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + amount + + + age + + + salary + + + repayment + + + goodhistory + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-4.pnmlx b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-4.pnmlx new file mode 100644 index 0000000..748d18d --- /dev/null +++ b/DataPetriNetOnSmt.Visualization/Samples_For_Import/bpmn-example-4.pnmlx @@ -0,0 +1,250 @@ + + + + + Credit Bank Request + + + + + i + + + 1 + + + + + p1 + + + + + p2 + + + + + p3 + + + + + p4 + + + + + p5 + + + + + p6 + + + + + p7 + + + + + p8 + + + + + o + + + 1 + + + + + Loan Request + + + + + AndS + + + + + Repayment Computation + + + + + History Evaluation + + + + + AndJ + + + + + Early Rejection + + + + + Preliminary Approval + + + + + Detailed Investigation + + + + + Rejection + + + + + + Loan Issue + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + 1 + + + + + + 1 + + + + + + amount + + + age + + + salary + + + repayment + + + goodhistory + + + + \ No newline at end of file diff --git a/DataPetriNetOnSmt/SoundnessVerification/Services/Repairment.cs b/DataPetriNetOnSmt/SoundnessVerification/Services/Repairment.cs index 30a203a..d6bef32 100644 --- a/DataPetriNetOnSmt/SoundnessVerification/Services/Repairment.cs +++ b/DataPetriNetOnSmt/SoundnessVerification/Services/Repairment.cs @@ -23,7 +23,7 @@ public Repairment() transformerToRefined = new TransformerToRefined(); } - public (DataPetriNet dpn, bool result) RepairDpn(DataPetriNet sourceDpn, bool mergeTransitionsBack = true) + public (DataPetriNet dpn, int repairSteps, bool result) RepairDpn(DataPetriNet sourceDpn, bool mergeTransitionsBack = true) { // Perform until stabilization // Termination - either if all are green or all are red @@ -39,7 +39,7 @@ public Repairment() HashSet transitionsToTrySimplify= new HashSet(); var transitionsDict = dpnToConsider.Transitions.ToDictionary(x => x.Id, y => y); - //var dpnBeforeLastRefinement = dpnToConsider; + var repairSteps = 0; do { @@ -81,11 +81,14 @@ public Repairment() if (!allNodesGreen && !allNodesRed) { (dpnToConsider, transitionsUpdatedAtPreviousStep) = MakeRepairStep(dpnToConsider, coloredCoverabilityTree, transitionsDict); + repairSteps++; transitionsToTrySimplify = transitionsToTrySimplify.Union(transitionsUpdatedAtPreviousStep).ToHashSet(); } else { RemoveDeadTransitions(dpnToConsider, coloredCoverabilityTree); + + return (dpnToConsider,0, allNodesGreen); } } else @@ -100,6 +103,7 @@ public Repairment() { transitionsToTrySimplify = transitionsToTrySimplify.Union(transitionsUpdatedAtPreviousStep).ToHashSet(); (dpnToConsider, transitionsUpdatedAtPreviousStep) = MakeRepairStep(dpnToConsider, coloredConstraintGraph, transitionsDict); + repairSteps++; transitionsToTrySimplify = transitionsToTrySimplify.Except(transitionsUpdatedAtPreviousStep).ToHashSet(); TryRollbackTransitionGuards(dpnToConsider, coloredConstraintGraph, transitionsToTrySimplify, transitionsDict); @@ -131,7 +135,7 @@ public Repairment() ? dpnToConsider : sourceDpn; - return (resultDpn, repairmentSuccessfullyFinished); + return (resultDpn, repairSteps, repairmentSuccessfullyFinished); static void RemoveIsolatedPlaces(DataPetriNet sourceDpn) diff --git a/DataPetriNetVerificationApplication/DataPetriNetVerificationApplication.csproj b/DataPetriNetVerificationApplication/DataPetriNetVerificationApplication.csproj index 680f8dd..5699862 100644 --- a/DataPetriNetVerificationApplication/DataPetriNetVerificationApplication.csproj +++ b/DataPetriNetVerificationApplication/DataPetriNetVerificationApplication.csproj @@ -5,10 +5,12 @@ net6.0 enable enable + AnyCPU;x64 + diff --git a/DataPetriNetVerificationApplication/Program.cs b/DataPetriNetVerificationApplication/Program.cs index 68179cf..548995d 100644 --- a/DataPetriNetVerificationApplication/Program.cs +++ b/DataPetriNetVerificationApplication/Program.cs @@ -1,6 +1,7 @@ using CsvHelper; using DataPetriNetOnSmt; using DataPetriNetOnSmt.Abstractions; +using DataPetriNetOnSmt.Enums; using DataPetriNetOnSmt.SoundnessVerification; using DataPetriNetOnSmt.SoundnessVerification.Services; using DataPetriNetOnSmt.SoundnessVerification.TransitionSystems; @@ -151,6 +152,10 @@ static int Main(string[] args) } } + ConductSoundnessRepair(dpnToVerify, soundnessProps, out var repairTime, out var result); + + satisfiesConditions &= repairTime != -1; + outputRow = new OptimizedVerificationOutput( dpnToVerify, satisfiesConditions, @@ -160,7 +165,9 @@ static int Main(string[] args) soundnessProps, ltsTime, cgTime, - cgRefinedTime); + cgRefinedTime, + repairTime, + result); } if (verificationAlgorithmType == VerificationAlgorithmTypeEnum.DirectVersion) { @@ -186,7 +193,11 @@ static int Main(string[] args) soundnessProps = LtsAnalyzer.CheckSoundness(dpnToVerify, lts); satisfiesConditions = VerifyConditions(conditionsInfo, dpnToVerify.Transitions.Count, soundnessProps); } - + + ConductSoundnessRepair(dpnToVerify, soundnessProps, out var repairTime, out var result); + + satisfiesConditions &= repairTime != -1; + outputRow = new BasicVerificationOutput( dpnToVerify, satisfiesConditions, @@ -195,7 +206,9 @@ static int Main(string[] args) soundnessProps, ltsTime, transformationTime, - cgRefinedTime); + cgRefinedTime, + repairTime, + result); } }, source.Token); if (!verificationTask.Wait(TimeSpan.FromMinutes(120))) @@ -225,6 +238,25 @@ static int Main(string[] args) return -1; } + private static void ConductSoundnessRepair(DataPetriNet dpnToVerify, SoundnessProperties? soundnessProps, out long repairTime, out bool result) + { + repairTime = -1; + result = false; + if (soundnessProps.StateTypes.Any(state => state.Value == ConstraintStateType.Final)) + { + var dpnRepairment = new Repairment(); + + var repairStopwatch = new Stopwatch(); + repairStopwatch.Start(); + + (_, var repairSteps, result) = dpnRepairment.RepairDpn(dpnToVerify); + + repairStopwatch.Stop(); + + repairTime = repairStopwatch.ElapsedMilliseconds; + } + } + private static DataPetriNet GetDpnToVerify(string dpnFilePath) { var xDoc = new XmlDocument(); diff --git a/DataPetriNetVerificationDomain/DataPetriNetVerificationDomain.csproj b/DataPetriNetVerificationDomain/DataPetriNetVerificationDomain.csproj index 6a3e07c..a24db5f 100644 --- a/DataPetriNetVerificationDomain/DataPetriNetVerificationDomain.csproj +++ b/DataPetriNetVerificationDomain/DataPetriNetVerificationDomain.csproj @@ -8,6 +8,7 @@ + diff --git a/DataPetriNetVerificationDomain/VerificationOutput.cs b/DataPetriNetVerificationDomain/VerificationOutput.cs index 7cc2202..1a76099 100644 --- a/DataPetriNetVerificationDomain/VerificationOutput.cs +++ b/DataPetriNetVerificationDomain/VerificationOutput.cs @@ -29,6 +29,8 @@ public class MainVerificationInfo public string VerificationTime { get; init; } public string LtsTime { get; init; } public string CgRefTime { get; init; } + public string? RepairTime { get; init; } + public bool? RepairSuccess { get; init; } public string Id { get; init; } public MainVerificationInfo() { @@ -53,6 +55,8 @@ public MainVerificationInfo(MainVerificationInfo verificationOutput) VerificationTime = verificationOutput.VerificationTime; LtsTime = verificationOutput.LtsTime; CgRefTime = verificationOutput.CgRefTime; + RepairTime = verificationOutput.RepairTime; + RepairSuccess = verificationOutput.RepairSuccess; Id = verificationOutput.Id; } public MainVerificationInfo(BasicVerificationOutput verificationOutput) @@ -74,6 +78,8 @@ public MainVerificationInfo(BasicVerificationOutput verificationOutput) VerificationTime = verificationOutput.VerificationTime; LtsTime = verificationOutput.LtsTime; CgRefTime = verificationOutput.CgRefTime; + RepairTime = verificationOutput.RepairTime; + RepairSuccess = verificationOutput.RepairSuccess; Id = verificationOutput.Id; } public MainVerificationInfo(OptimizedVerificationOutput verificationOutput) @@ -95,6 +101,8 @@ public MainVerificationInfo(OptimizedVerificationOutput verificationOutput) VerificationTime = verificationOutput.VerificationTime; LtsTime = verificationOutput.LtsTime; CgRefTime = verificationOutput.CgRefTime; + RepairTime = verificationOutput.RepairTime; + RepairSuccess = verificationOutput.RepairSuccess; Id = verificationOutput.Id; } } @@ -110,7 +118,9 @@ public BasicVerificationOutput( SoundnessProperties? soundnessProperties, long millisecondsForLts, long millisecondsForTransformation, - long millisecondsForCgRefined) + long millisecondsForCgRefined, + long millisecondsForRepair, + bool repairSuccess) { Places = (ushort)dpn.Places.Count; Transitions = (ushort)dpn.Transitions.Count; @@ -134,6 +144,8 @@ public BasicVerificationOutput( CgRefTime = millisecondsForCgRefined.ToString(); CgRefArcs = cgRefined?.ConstraintArcs.Count ?? -1; CgRefStates = cgRefined?.ConstraintStates.Count ?? -1; + RepairTime = millisecondsForRepair.ToString(); + RepairSuccess = repairSuccess; } public BasicVerificationOutput() { @@ -160,7 +172,9 @@ public OptimizedVerificationOutput( SoundnessProperties? soundnessProperties, long millisecondsForLts, long millisecondsForCg, - long millisecondsForCgRefined) + long millisecondsForCgRefined, + long millisecondsForRepair, + bool repairSuccess) { Places = (ushort)dpn.Places.Count; Transitions = (ushort)dpn.Transitions.Count; @@ -187,6 +201,8 @@ public OptimizedVerificationOutput( CgRefTime = millisecondsForCgRefined.ToString(); CgRefArcs = cgRefined?.ConstraintArcs?.Count ?? -1; CgRefStates= cgRefined?.ConstraintStates?.Count ?? -1; + RepairTime = millisecondsForRepair.ToString(); + RepairSuccess = repairSuccess; } } public class VerificationOutputWithNumber : MainVerificationInfo @@ -216,6 +232,8 @@ public VerificationOutputWithNumber(MainVerificationInfo verificationOutput, int Id = verificationOutput.Id; LtsTime = verificationOutput.LtsTime; CgRefTime = verificationOutput.CgRefTime; + RepairTime = verificationOutput.RepairTime; + RepairSuccess = verificationOutput.RepairSuccess; //VerificationType = verificationOutput.VerificationType; } } diff --git a/ToGraphParser/DataPetriNetParsers.csproj b/ToGraphParser/DataPetriNetParsers.csproj index fe773ec..47e3f45 100644 --- a/ToGraphParser/DataPetriNetParsers.csproj +++ b/ToGraphParser/DataPetriNetParsers.csproj @@ -9,6 +9,7 @@ + diff --git a/ToGraphParser/PnmlParser.cs b/ToGraphParser/PnmlParser.cs index e8dc9a6..51bb347 100644 --- a/ToGraphParser/PnmlParser.cs +++ b/ToGraphParser/PnmlParser.cs @@ -5,6 +5,7 @@ using Microsoft.Z3; using System; using System.Collections.Generic; +using System.Globalization; using System.Linq; using System.Xml; using System.Xml.Linq; @@ -145,6 +146,8 @@ public DataPetriNet DeserializeDpn(XmlDocument document) { } + var t = dpn.Arcs.GroupBy(x => x.Destination.Id); + return dpn; } @@ -342,7 +345,7 @@ private IConstraintExpression FormConstraint(Dictionary varT GetBinaryPredicate(constraintBlocks[1]), variableName, variableType, - double.Parse(constraintBlocks[2])), + double.Parse(constraintBlocks[2], CultureInfo.InvariantCulture)), DomainType.Boolean => MakeVOCConstraint( varTypeDict[variableName],