diff --git a/btypes_primitives/src/main/rust/btypes/src/brelation.rs b/btypes_primitives/src/main/rust/btypes/src/brelation.rs index 1153cf4706de600dc0f4082c2cc32d4fa628db52..690f506fc88e39b870a024cf9bb61ddc0cdc41cf 100644 --- a/btypes_primitives/src/main/rust/btypes/src/brelation.rs +++ b/btypes_primitives/src/main/rust/btypes/src/brelation.rs @@ -422,12 +422,6 @@ impl<L: 'static + BObject, R: 'static + BObject> BRelation<L, R> { rel.update_unit(key.clone(), BSet::fromOrdSet(range.clone()))) } - pub fn cartesianProduct(set_a: &BSet<L>, set_b: &BSet<R>) -> BRelation<L, R> { - // slightly inefficient due to double iteration - return BSet::<L>::cartesian::<L, R>(&set_a.as_ord_set(), &set_b.as_ord_set()).iter() - .fold(BRelation::new(vec![]), |mut rel, tuple| { rel.insert(tuple); return rel; }); - } - pub fn nondeterminism(&self) -> BTuple<L, R> { let mut rng = rand::thread_rng(); let tuple = self.map.iter().choose(&mut rng).unwrap(); @@ -664,8 +658,28 @@ impl<L, R> BRelation<L, R> pub fn checkRangeStruct(&self) -> BBoolean { return BBoolean::new(true); } } +impl<L, R> BRelation<L, R> + where L: 'static + SetLike, + R: 'static + SetLike { + + pub fn cartesianProduct(set_a: &L, set_b: &R) -> BRelation<L::Item, R::Item> { + // slightly inefficient due to double iteration, more if BRelation parameter + return BSet::<L::Item>::cartesian::<L::Item, R::Item>(&set_a.as_bset().as_ord_set(), &set_b.as_bset().as_ord_set()).iter() + .fold(BRelation::new(vec![]), |mut rel, tuple| { rel.insert(tuple); return rel; }); + } +} + impl<L: 'static + BObject, R: 'static + BObject> SetLike for BRelation<L, R> { + type Item = BTuple<L, R>; + fn get_empty() -> Self { BRelation::<L, R>::new(vec![]) } fn _union(&self, other: &Self) -> Self { self._union(other) } fn intersect(&self, other: &Self) -> Self { self.intersect(other) } + fn as_bset(&self) -> BSet<BTuple<L, R>> { + BSet::fromOrdSet( + self.map.iter().fold(OrdSet::new(), |mut acc, (key, values)| { + values.iter().for_each(|v| { acc.insert(BTuple::from_refs(key, v)); }); + return acc; + })) + } } diff --git a/btypes_primitives/src/main/rust/btypes/src/bset.rs b/btypes_primitives/src/main/rust/btypes/src/bset.rs index 0d0147b5d226a84aac55754b0c4933f93473b9d5..ffe05dd2f2df125f5657b9a80c7f940be0ce06b7 100644 --- a/btypes_primitives/src/main/rust/btypes/src/bset.rs +++ b/btypes_primitives/src/main/rust/btypes/src/bset.rs @@ -24,9 +24,12 @@ pub trait TBSet: BObject { } pub trait SetLike: BObject { + type Item: BObject; + fn get_empty() -> Self; fn _union(&self, other: &Self) -> Self; fn intersect(&self, other: &Self) -> Self; + fn as_bset(&self) -> BSet<Self::Item>; } #[derive(Default, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, Clone)] @@ -377,9 +380,14 @@ impl<T: 'static + BInt> BSet<T> { } impl<T: 'static + BObject> SetLike for BSet<T> { + type Item = T; + fn get_empty() -> Self { BSet::<T>::new(vec![]) } fn _union(&self, other: &Self) -> Self { self._union(other) } fn intersect(&self, other: &Self) -> Self { self.intersect(other) } + fn as_bset(&self) -> BSet<T> { + return self.clone(); + } } impl<T: 'static + SetLike> BSet<T> { diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg index c7c6468c22c7dcd0e5b87830d2ac8e7df8753d4d..015959be2a719d768e92332d126cf7c7dd1b923f 100644 --- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg +++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg @@ -441,7 +441,7 @@ impl fmt::Display for <name> { >> bool() ::= << -butils::BOOL +(*butils::BOOL) >> include_declaration(type, identifier) ::= << diff --git a/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch b/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch new file mode 100644 index 0000000000000000000000000000000000000000..c82b411c51d806c0154f827406c8b6f9fa8edf66 --- /dev/null +++ b/src/test/resources/de/hhu/stups/codegenerator/SetRelationConstructs.mch @@ -0,0 +1,20 @@ +MACHINE SetRelationConstructs +VARIABLES basea, a, baseb, b, basec, c +INVARIANT + basea : POW(BOOL * BOOL * BOOL) & + a: basea & + baseb: POW(BOOL * (BOOL * BOOL)) & + b: baseb & + basec: POW((BOOL * BOOL) * (BOOL * BOOL)) & + c: basec + + +INITIALISATION + basea:=BOOL*BOOL*BOOL; a:=(TRUE |-> FALSE) |-> TRUE; + baseb:=BOOL*(BOOL*BOOL); b:=TRUE |-> (FALSE |-> TRUE); + basec:=(BOOL*BOOL)*(BOOL*BOOL); c:=(TRUE |-> FALSE) |-> (TRUE |-> TRUE) + +OPERATIONS + AssertionsOK = PRE ( TRUE : BOOL) THEN skip END +END +