Skip to content

Commit

Permalink
Small updates
Browse files Browse the repository at this point in the history
  • Loading branch information
nm.suvorov committed Nov 4, 2024
1 parent 472c67e commit c82960f
Show file tree
Hide file tree
Showing 38 changed files with 7,679 additions and 31 deletions.
3 changes: 2 additions & 1 deletion .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -360,4 +360,5 @@ MigrationBackup/
.ionide/

# Fody - auto-generated XML schema
FodyWeavers.xsd
FodyWeavers.xsd
/.idea/.idea.DataPetriNet/.idea
50 changes: 42 additions & 8 deletions DataPetriNet.sln
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions DataPetriNetGeneration/DataPetriNetGeneration.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@
<Platforms>AnyCPU;x86;x64</Platforms>
</PropertyGroup>

<ItemGroup>
<PackageReference Include="Microsoft.Z3" Version="4.12.2" />
</ItemGroup>

<ItemGroup>
<ProjectReference Include="..\DataPetriNetOnSmt\DataPetriNetOnSmt.csproj" />
</ItemGroup>
Expand Down
4 changes: 2 additions & 2 deletions DataPetriNetIterativeVerificationApplication/Configuration.json
View file
Original file line number Diff line number Diff line change
@@ -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\\"
}
4 changes: 3 additions & 1 deletion ...riNetIterativeVerificationApplication/DataPetriNetIterativeVerificationApplication.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
<TargetFramework>net6.0-windows</TargetFramework>
<Nullable>enable</Nullable>
<UseWPF>true</UseWPF>
<Platforms>AnyCPU;x86;x64</Platforms>
</PropertyGroup>

<ItemGroup>
Expand All @@ -17,6 +18,7 @@
<PackageReference Include="AutomaticGraphLayout.Drawing" Version="1.1.12" />
<PackageReference Include="AutomaticGraphLayout.WpfGraphControl" Version="1.1.12" />
<PackageReference Include="Enums.NET" Version="4.0.0" />
<PackageReference Include="Microsoft.Z3" Version="4.12.2" />
<PackageReference Include="Newtonsoft.Json" Version="13.0.1" />
</ItemGroup>

Expand All @@ -34,7 +36,7 @@

<ItemGroup>
<None Update="Configuration.json">
<CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
<CopyToOutputDirectory>Always</CopyToOutputDirectory>
</None>
</ItemGroup>

Expand Down
4 changes: 3 additions & 1 deletion DataPetriNetIterativeVerificationApplication/MainWindow.xaml.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ public partial class MainWindow : Window
private Dictionary<int, string> paths = new Dictionary<int, string>();
private ObservableCollection<VerificationOutputWithNumber> verificationResults = new();
private CancellationTokenSource source;
private VerificationRunner verificationRunner = new();
private VerificationRunner verificationRunner;
public MainWindow()
{
InitializeComponent();
Expand Down Expand Up @@ -75,6 +75,8 @@ public MainWindow()
MaxConditionsTb.Text = "150";
MaxVarsTb.Text = "150";

verificationRunner = new();

VerificationDG.ItemsSource = verificationResults;
verificationResults.CollectionChanged += listChanged;
}
Expand Down
12 changes: 6 additions & 6 deletions DataPetriNetIterativeVerificationApplication/Services/IterativeVerificationRunner.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ public async Task RunIterativeVerificationLoop(
var verificationTypes = new List<VerificationAlgorithmTypeEnum>
{
VerificationAlgorithmTypeEnum.ImprovedVersion,
VerificationAlgorithmTypeEnum.DirectVersion
//VerificationAlgorithmTypeEnum.DirectVersion
};

do
Expand All @@ -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();

Expand Down
1 change: 1 addition & 0 deletions DataPetriNetOnSmt.Tests/DataPetriNetOnSmt.Tests.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@

<ItemGroup>
<PackageReference Include="Microsoft.NET.Test.Sdk" Version="16.11.0" />
<PackageReference Include="Microsoft.Z3" Version="4.12.2" />
<PackageReference Include="MSTest.TestAdapter" Version="2.2.7" />
<PackageReference Include="MSTest.TestFramework" Version="2.2.7" />
<PackageReference Include="coverlet.collector" Version="3.1.0" />
Expand Down
1 change: 1 addition & 0 deletions DataPetriNetOnSmt.Visualization/DataPetriNetOnSmt.Visualization.csproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
<PackageReference Include="AutomaticGraphLayout.Drawing" Version="1.1.12" />
<PackageReference Include="AutomaticGraphLayout.WpfGraphControl" Version="1.1.12" />
<PackageReference Include="Enums.NET" Version="4.0.0" />
<PackageReference Include="Microsoft.Z3" Version="4.12.2" />
<PackageReference Include="System.Collections" Version="4.3.0" />
</ItemGroup>

Expand Down
6 changes: 3 additions & 3 deletions DataPetriNetOnSmt.Visualization/MainWindow.xaml.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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);
}
}
Expand Down
Loading

0 comments on commit c82960f

Please sign in to comment.