diff --git a/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs b/btypes_primitives/src/main/rust/btypes/src/OrderedHashSet.rs index 66a313ec3803ceda4697fee55f413a7593372b11..2680018b8716deff8f20ad27b0f484f7ef949a51 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 efca05dd513617c1f15a0fe6417528a8724ed731..d1eab3dffa1067b36e38952b53c5f77198e25e49 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 29c6512c44a252b268af698c916016463cb5b622..b0171b192148a704bdf536336b034fd3e8576426 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 c9191f8df11b7208724fb41a0eb5284f3ea52c97..a316ad0ed80c35070b64fddffe544aec49c2d7d8 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 3c8a8788917b65f40b81428e9e0f61f33c8aa093..4716d4ce0f85e0d3634953a4aa073d71ff254744 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 b43e5265891d26c1bcd3b3c60cbc7a587ac4d8e6..69e29a97976280352deb092bd1920186d6ca0129 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 6e70cf0df585ff0d85c8244faaa1d19005906d00..dbc0a88c7e65a3221501236d5d833ea691930229 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 826bc9bfc7edfe82a79172a34ca592589c8d1a82..ff5504b894bc52836725e96b9c5aa39b6387167c 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 9a0820642eb0f88f48f91662d31834a84b9eb1b2..cdab9af7d103feaa7f788086a4915c638620e08b 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