From 6219832e161146f77d7729b595cf359f785f32bd Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Mon, 21 Mar 2022 15:34:47 +0100
Subject: [PATCH] fixed some btype and template bugs
---
.../main/rust/btypes/src/OrderedHashSet.rs | 46 ++++++++++++++++++-
.../src/main/rust/btypes/src/brelation.rs | 38 ++++++++++++++-
.../hhu/stups/codegenerator/RustTemplate.stg | 35 ++++++--------
.../codegenerator/rust/TestMCBenchmarks.java | 8 ++--
.../codegenerator/Train1_Lukas_POR_v3_MC.out | 4 +-
...rain_1_beebook_deterministic_MC_POR_v2.out | 4 +-
.../landing_gear/LandingGear_R6_MC.out | 2 +-
.../de/hhu/stups/codegenerator/nota_v2_MC.out | 2 +-
.../codegenerator/sort_m2_data1000_MC.out | 2 +-
9 files changed, 107 insertions(+), 34 deletions(-)
diff --git a/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
index 66a313ec3..2680018b8 100644
--- a/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs
@@ -1,18 +1,60 @@
use std::borrow::Borrow;
use std::collections::hash_map::DefaultHasher;
use std::cell::RefCell;
+use std::cmp::Ordering;
use std::hash::{Hash, Hasher};
use im::OrdSet;
use im::ordset::Iter;
use crate::bobject::BObject;
-#[derive(Default, Debug, Eq, PartialOrd, Ord, Clone)]
+#[derive(Default, Debug, Eq)]
pub struct OrderedHashSet<I: BObject> {
set: OrdSet<I>,
hash_cache: RefCell<Option<u64>>,
}
+impl<I: BObject> Clone for OrderedHashSet<I> {
+ fn clone(&self) -> Self {
+ OrderedHashSet { set: self.set.clone(), hash_cache: RefCell::new(self.hash_cache.borrow().clone()) }
+ }
+}
+
+impl<I: BObject> PartialOrd for OrderedHashSet<I> {
+ fn partial_cmp(&self, other: &Self) -> Option<Ordering> { self.set.partial_cmp(&other.set) }
+ fn lt(&self, other: &Self) -> bool { self.set.lt(&other.set) }
+ fn le(&self, other: &Self) -> bool { self.set.le(&other.set) }
+ fn gt(&self, other: &Self) -> bool { self.set.gt(&other.set) }
+ fn ge(&self, other: &Self) -> bool { self.set.ge(&other.set) }
+}
+
+impl<I: BObject> Ord for OrderedHashSet<I> {
+ fn cmp(&self, other: &Self) -> Ordering { self.set.cmp(&other.set) }
+ fn max(self, other: Self) -> Self {
+ match self.cmp(&other) {
+ Ordering::Less => other,
+ Ordering::Greater => self,
+ Ordering::Equal => other,
+ }
+ }
+ fn min(self, other: Self) -> Self {
+ match self.cmp(&other) {
+ Ordering::Less => self,
+ Ordering::Greater => other,
+ Ordering::Equal => self,
+ }
+ }
+ fn clamp(self, min: Self, max: Self) -> Self {
+ if self < min {
+ min
+ } else if self > max {
+ max
+ } else {
+ self
+ }
+ }
+}
+
//TODO: check if replacing cache with mutex works and does not impact permormance too much
unsafe impl<T: BObject> Sync for OrderedHashSet<T> {}
@@ -24,7 +66,7 @@ impl<I: BObject> PartialEq for OrderedHashSet<I> {
impl<I: BObject> Hash for OrderedHashSet<I> {
fn hash<H: Hasher>(self: &OrderedHashSet<I>, state: &mut H) {
- let cache = self.hash_cache.clone().take();
+ let cache = self.hash_cache.borrow().clone();
let hash: u64;
if cache.is_none() {
diff --git a/btypes_primitives/src/main/rust/btypes/src/brelation.rs b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
index efca05dd5..d1eab3dff 100644
--- a/btypes_primitives/src/main/rust/btypes/src/brelation.rs
+++ b/btypes_primitives/src/main/rust/btypes/src/brelation.rs
@@ -3,6 +3,7 @@
use std::collections::hash_map::DefaultHasher;
use std::collections::LinkedList;
use std::cell::RefCell;
+use std::cmp::Ordering;
use crate::bobject::BObject;
use crate::binteger::{BInt, BInteger, FromBInt};
use crate::btuple::BTuple;
@@ -25,12 +26,47 @@ enum CombiningType {
UNION
}
-#[derive(Default, Debug, Eq, PartialOrd, Ord, Clone)]
+#[derive(Default, Debug, Eq, Clone)]
pub struct BRelation<L: BObject, R: BObject> {
map: HashMap<L, OrdSet<R>>,
hash_cache: RefCell<Option<u64>>,
}
+impl<L: BObject, R: BObject> PartialOrd for BRelation<L, R> {
+ fn partial_cmp(&self, other: &Self) -> Option<Ordering> { self.map.partial_cmp(&other.map) }
+ fn lt(&self, other: &Self) -> bool { self.map.lt(&other.map) }
+ fn le(&self, other: &Self) -> bool { self.map.le(&other.map) }
+ fn gt(&self, other: &Self) -> bool { self.map.gt(&other.map) }
+ fn ge(&self, other: &Self) -> bool { self.map.ge(&other.map) }
+}
+
+impl<L: BObject, R: BObject> Ord for BRelation<L, R> {
+ fn cmp(&self, other: &Self) -> Ordering { self.map.cmp(&other.map) }
+ fn max(self, other: Self) -> Self {
+ match self.cmp(&other) {
+ Ordering::Less => other,
+ Ordering::Greater => self,
+ Ordering::Equal => other,
+ }
+ }
+ fn min(self, other: Self) -> Self {
+ match self.cmp(&other) {
+ Ordering::Less => self,
+ Ordering::Greater => other,
+ Ordering::Equal => self,
+ }
+ }
+ fn clamp(self, min: Self, max: Self) -> Self {
+ if self < min {
+ min
+ } else if self > max {
+ max
+ } else {
+ self
+ }
+ }
+}
+
//TODO: check if replacing cache with mutex works and does not impact permormance too much
unsafe impl<L: BObject, R: BObject> Sync for BRelation<L, R> {}
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index 29c6512c4..b0171b192 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -3,7 +3,7 @@ as, break, const, continue, crate, else, enum, extern, false, fn, for, if, impl,
>>
-machine(imports, includedMachines, machine, structs, constants_declarations, includes, enums, sets, declarations, initialization, operations, addition, useBigInteger, getters, lambdaFunctions, forModelChecking, transitions, invariant, copy, modelcheck, transitionCachesDeclaration) ::= <<
+machine(imports, includedMachines, machine, structs, constants_declarations, includes, enums, sets, declarations, initialization, operations, addition, useBigInteger, getters, lambdaFunctions, forModelChecking, transitions, invariant, copy, modelcheck, transitionCachesDeclaration, hash_equal) ::= <<
#![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
<if(forModelChecking)>
use std::env;
@@ -46,6 +46,8 @@ pub struct <machine> {
<transitionCachesDeclaration; separator="\n#[derivative(Hash=\"ignore\", PartialEq=\"ignore\")]\n"><endif>
}
+<hash_equal>
+
impl <machine> {
<initialization>
<if(getters)><\n><getters; separator="\n\n"><endif>
@@ -97,7 +99,7 @@ import_type(type, useBigInteger) ::= <<
use btypes::<type; format="lower">::<type>;
>>
-initialization(machine, properties, values, body, sets, set_initializations, includesInitialization) ::= <<
+initialization(machine, properties, values, body, set_initializations, includesInitialization) ::= <<
pub fn new() -> <machine> {
<if(values)> //values: '<values>'<endif>
@@ -106,9 +108,8 @@ pub fn new() -> <machine> {
return m;
}
fn init(&mut self) {
- <properties; separator="\n">
- <sets; separator="\n">
<set_initializations; separator="\n">
+ <properties; separator="\n">
<body>
<includesInitialization; separator="\n">
}
@@ -124,7 +125,7 @@ identifier(machine, identifier, isReturn, isPrivate, isLocal, isParam, isAssigne
>>
getter(returnType, isConstant, machine, variable) ::= <<
-pub fn get_<variable>(&self) -> <returnType> {
+pub fn _get_<variable>(&self) -> <returnType> {
return self.<variable>.clone();
}
>>
@@ -728,27 +729,21 @@ mc_info_type(<isSet>, <machine>, <type>)
>>
machine_equal() ::= <<
-machine_equal()
>>
machine_unequal() ::= <<
-machine_equal()
>>
machine_equal_predicate() ::= <<
-machine_equal_predicate()
>>
machine_unequal_predicate() ::= <<
-machine_equal_predicate()
>>
machine_hash() ::= <<
-machine_hash()
>>
machine_hash_assignment() ::= <<
-machine_hash_assignment()
>>
enum_import() ::= <<
@@ -809,6 +804,7 @@ model_check_invariant(invariant) ::= <<
//model_check_invariant
if dependent_invariants_of_state.contains(&"<invariant>") {
if !state.<invariant>() {
+ println!("<invariant> failed!");
return false;
}
}
@@ -1073,15 +1069,14 @@ fn invalidate_caches(&mut self, to_invalidate: Vec\<&'static str>) {
}
>>
-machine_string(variables) ::= <<
-@Override
-public String toString() {
- //machine_string
- <if(variables)>
- return String.join("\n", <variables:{var | "<var>: " + (this.<var>()).toString()}; separator=", ">);
- <else>
- return "";
- <endif>
+machine_string(variables, machine) ::= <<
+impl fmt::Display for <machine> {
+ fn fmt(&self, f: &mut fmt::Formatter\<'_>) -> fmt::Result {
+ let mut result = "<machine>: (".to_owned();
+ <variables:{var | result += &format!("<var>: <\u007B><\u007D>, ", self.<var>());}; separator="\n">
+ result = result + ")";
+ return write!(f, "{}", result);
+ }
}
>>
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java
index c9191f8df..a316ad0ed 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestMCBenchmarks.java
@@ -45,12 +45,12 @@ public class TestMCBenchmarks extends TestRS {
}
@Test
- public void testTrain1_Lukas_POR() throws Exception {
- testRSMC("Train1_Lukas_POR");
+ public void testTrain1_Lukas_POR_v3() throws Exception {
+ testRSMC("Train1_Lukas_POR_v3");
}
@Test
- public void testTrain_1_beebook_deterministic_MC_POR() throws Exception {
- testRSMC("Train_1_beebook_deterministic_MC_POR", false);
+ public void testTrain_1_beebook_deterministic_MC_POR_v2() throws Exception {
+ testRSMC("Train_1_beebook_deterministic_MC_POR_v2");
}
}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train1_Lukas_POR_v3_MC.out b/src/test/resources/de/hhu/stups/codegenerator/Train1_Lukas_POR_v3_MC.out
index 3c8a87889..4716d4ce0 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train1_Lukas_POR_v3_MC.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train1_Lukas_POR_v3_MC.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
-Number of States: 24636
-Number of Transitions:
\ No newline at end of file
+Number of States: 24635
+Number of Transitions: 55368
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.out b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.out
index b43e52658..69e29a979 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/Train_1_beebook_deterministic_MC_POR_v2.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
-Number of States: 672175
-Number of Transitions:
\ No newline at end of file
+Number of States: 672173
+Number of Transitions: 2244484
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6_MC.out b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6_MC.out
index 6e70cf0df..dbc0a88c7 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6_MC.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/landing_gear/LandingGear_R6_MC.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
Number of States: 131328
-Number of Transitions: 884369
\ No newline at end of file
+Number of Transitions: 884368
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/nota_v2_MC.out b/src/test/resources/de/hhu/stups/codegenerator/nota_v2_MC.out
index 826bc9bfc..ff5504b89 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/nota_v2_MC.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/nota_v2_MC.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
Number of States: 80718
-Number of Transitions: 1797353
\ No newline at end of file
+Number of Transitions: 1797352
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.out b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.out
index 9a0820642..cdab9af7d 100644
--- a/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.out
+++ b/src/test/resources/de/hhu/stups/codegenerator/sort_m2_data1000_MC.out
@@ -1,3 +1,3 @@
MODEL CHECKING SUCCESSFUL
Number of States: 500501
-Number of Transitions: 500502
\ No newline at end of file
+Number of Transitions: 500500
\ No newline at end of file
--
GitLab