Skip to content
Snippets Groups Projects
Commit 6219832e authored by Cookiebowser's avatar Cookiebowser
Browse files

fixed some btype and template bugs

parent 57695cfd
No related branches found
No related tags found
1 merge request!28Rust support
Showing with 107 additions and 34 deletions
use std::borrow::Borrow; use std::borrow::Borrow;
use std::collections::hash_map::DefaultHasher; use std::collections::hash_map::DefaultHasher;
use std::cell::RefCell; use std::cell::RefCell;
use std::cmp::Ordering;
use std::hash::{Hash, Hasher}; use std::hash::{Hash, Hasher};
use im::OrdSet; use im::OrdSet;
use im::ordset::Iter; use im::ordset::Iter;
use crate::bobject::BObject; use crate::bobject::BObject;
#[derive(Default, Debug, Eq, PartialOrd, Ord, Clone)] #[derive(Default, Debug, Eq)]
pub struct OrderedHashSet<I: BObject> { pub struct OrderedHashSet<I: BObject> {
set: OrdSet<I>, set: OrdSet<I>,
hash_cache: RefCell<Option<u64>>, 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 //TODO: check if replacing cache with mutex works and does not impact permormance too much
unsafe impl<T: BObject> Sync for OrderedHashSet<T> {} unsafe impl<T: BObject> Sync for OrderedHashSet<T> {}
...@@ -24,7 +66,7 @@ impl<I: BObject> PartialEq for OrderedHashSet<I> { ...@@ -24,7 +66,7 @@ impl<I: BObject> PartialEq for OrderedHashSet<I> {
impl<I: BObject> Hash for OrderedHashSet<I> { impl<I: BObject> Hash for OrderedHashSet<I> {
fn hash<H: Hasher>(self: &OrderedHashSet<I>, state: &mut H) { 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; let hash: u64;
if cache.is_none() { if cache.is_none() {
......
...@@ -3,6 +3,7 @@ ...@@ -3,6 +3,7 @@
use std::collections::hash_map::DefaultHasher; use std::collections::hash_map::DefaultHasher;
use std::collections::LinkedList; use std::collections::LinkedList;
use std::cell::RefCell; use std::cell::RefCell;
use std::cmp::Ordering;
use crate::bobject::BObject; use crate::bobject::BObject;
use crate::binteger::{BInt, BInteger, FromBInt}; use crate::binteger::{BInt, BInteger, FromBInt};
use crate::btuple::BTuple; use crate::btuple::BTuple;
...@@ -25,12 +26,47 @@ enum CombiningType { ...@@ -25,12 +26,47 @@ enum CombiningType {
UNION UNION
} }
#[derive(Default, Debug, Eq, PartialOrd, Ord, Clone)] #[derive(Default, Debug, Eq, Clone)]
pub struct BRelation<L: BObject, R: BObject> { pub struct BRelation<L: BObject, R: BObject> {
map: HashMap<L, OrdSet<R>>, map: HashMap<L, OrdSet<R>>,
hash_cache: RefCell<Option<u64>>, 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 //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> {} unsafe impl<L: BObject, R: BObject> Sync for BRelation<L, R> {}
......
...@@ -3,7 +3,7 @@ as, break, const, continue, crate, else, enum, extern, false, fn, for, if, impl, ...@@ -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 ) ] #![ allow( dead_code, unused, non_snake_case, non_camel_case_types, unused_assignments ) ]
<if(forModelChecking)> <if(forModelChecking)>
use std::env; use std::env;
...@@ -46,6 +46,8 @@ pub struct <machine> { ...@@ -46,6 +46,8 @@ pub struct <machine> {
<transitionCachesDeclaration; separator="\n#[derivative(Hash=\"ignore\", PartialEq=\"ignore\")]\n"><endif> <transitionCachesDeclaration; separator="\n#[derivative(Hash=\"ignore\", PartialEq=\"ignore\")]\n"><endif>
} }
<hash_equal>
impl <machine> { impl <machine> {
<initialization> <initialization>
<if(getters)><\n><getters; separator="\n\n"><endif> <if(getters)><\n><getters; separator="\n\n"><endif>
...@@ -97,7 +99,7 @@ import_type(type, useBigInteger) ::= << ...@@ -97,7 +99,7 @@ import_type(type, useBigInteger) ::= <<
use btypes::<type; format="lower">::<type>; 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> { pub fn new() -> <machine> {
<if(values)> //values: '<values>'<endif> <if(values)> //values: '<values>'<endif>
...@@ -106,9 +108,8 @@ pub fn new() -> <machine> { ...@@ -106,9 +108,8 @@ pub fn new() -> <machine> {
return m; return m;
} }
fn init(&mut self) { fn init(&mut self) {
<properties; separator="\n">
<sets; separator="\n">
<set_initializations; separator="\n"> <set_initializations; separator="\n">
<properties; separator="\n">
<body> <body>
<includesInitialization; separator="\n"> <includesInitialization; separator="\n">
} }
...@@ -124,7 +125,7 @@ identifier(machine, identifier, isReturn, isPrivate, isLocal, isParam, isAssigne ...@@ -124,7 +125,7 @@ identifier(machine, identifier, isReturn, isPrivate, isLocal, isParam, isAssigne
>> >>
getter(returnType, isConstant, machine, variable) ::= << getter(returnType, isConstant, machine, variable) ::= <<
pub fn get_<variable>(&self) -> <returnType> { pub fn _get_<variable>(&self) -> <returnType> {
return self.<variable>.clone(); return self.<variable>.clone();
} }
>> >>
...@@ -728,27 +729,21 @@ mc_info_type(<isSet>, <machine>, <type>) ...@@ -728,27 +729,21 @@ mc_info_type(<isSet>, <machine>, <type>)
>> >>
machine_equal() ::= << machine_equal() ::= <<
machine_equal()
>> >>
machine_unequal() ::= << machine_unequal() ::= <<
machine_equal()
>> >>
machine_equal_predicate() ::= << machine_equal_predicate() ::= <<
machine_equal_predicate()
>> >>
machine_unequal_predicate() ::= << machine_unequal_predicate() ::= <<
machine_equal_predicate()
>> >>
machine_hash() ::= << machine_hash() ::= <<
machine_hash()
>> >>
machine_hash_assignment() ::= << machine_hash_assignment() ::= <<
machine_hash_assignment()
>> >>
enum_import() ::= << enum_import() ::= <<
...@@ -809,6 +804,7 @@ model_check_invariant(invariant) ::= << ...@@ -809,6 +804,7 @@ model_check_invariant(invariant) ::= <<
//model_check_invariant //model_check_invariant
if dependent_invariants_of_state.contains(&"<invariant>") { if dependent_invariants_of_state.contains(&"<invariant>") {
if !state.<invariant>() { if !state.<invariant>() {
println!("<invariant> failed!");
return false; return false;
} }
} }
...@@ -1073,15 +1069,14 @@ fn invalidate_caches(&mut self, to_invalidate: Vec\<&'static str>) { ...@@ -1073,15 +1069,14 @@ fn invalidate_caches(&mut self, to_invalidate: Vec\<&'static str>) {
} }
>> >>
machine_string(variables) ::= << machine_string(variables, machine) ::= <<
@Override impl fmt::Display for <machine> {
public String toString() { fn fmt(&self, f: &mut fmt::Formatter\<'_>) -> fmt::Result {
//machine_string let mut result = "<machine>: (".to_owned();
<if(variables)> <variables:{var | result += &format!("<var>: <\u007B><\u007D>, ", self.<var>());}; separator="\n">
return String.join("\n", <variables:{var | "<var>: " + (this.<var>()).toString()}; separator=", ">); result = result + ")";
<else> return write!(f, "{}", result);
return ""; }
<endif>
} }
>> >>
......
...@@ -45,12 +45,12 @@ public class TestMCBenchmarks extends TestRS { ...@@ -45,12 +45,12 @@ public class TestMCBenchmarks extends TestRS {
} }
@Test @Test
public void testTrain1_Lukas_POR() throws Exception { public void testTrain1_Lukas_POR_v3() throws Exception {
testRSMC("Train1_Lukas_POR"); testRSMC("Train1_Lukas_POR_v3");
} }
@Test @Test
public void testTrain_1_beebook_deterministic_MC_POR() throws Exception { public void testTrain_1_beebook_deterministic_MC_POR_v2() throws Exception {
testRSMC("Train_1_beebook_deterministic_MC_POR", false); testRSMC("Train_1_beebook_deterministic_MC_POR_v2");
} }
} }
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 24636 Number of States: 24635
Number of Transitions: Number of Transitions: 55368
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 672175 Number of States: 672173
Number of Transitions: Number of Transitions: 2244484
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 131328 Number of States: 131328
Number of Transitions: 884369 Number of Transitions: 884368
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 80718 Number of States: 80718
Number of Transitions: 1797353 Number of Transitions: 1797352
\ No newline at end of file \ No newline at end of file
MODEL CHECKING SUCCESSFUL MODEL CHECKING SUCCESSFUL
Number of States: 500501 Number of States: 500501
Number of Transitions: 500502 Number of Transitions: 500500
\ No newline at end of file \ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment