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

fixed CartesianProduct for Relation parameter

parent 101f55fb
Branches
No related tags found
1 merge request!28Rust support
...@@ -422,12 +422,6 @@ impl<L: 'static + BObject, R: 'static + BObject> BRelation<L, R> { ...@@ -422,12 +422,6 @@ impl<L: 'static + BObject, R: 'static + BObject> BRelation<L, R> {
rel.update_unit(key.clone(), BSet::fromOrdSet(range.clone()))) 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> { pub fn nondeterminism(&self) -> BTuple<L, R> {
let mut rng = rand::thread_rng(); let mut rng = rand::thread_rng();
let tuple = self.map.iter().choose(&mut rng).unwrap(); let tuple = self.map.iter().choose(&mut rng).unwrap();
...@@ -664,8 +658,28 @@ impl<L, R> BRelation<L, R> ...@@ -664,8 +658,28 @@ impl<L, R> BRelation<L, R>
pub fn checkRangeStruct(&self) -> BBoolean { return BBoolean::new(true); } 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> { 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 get_empty() -> Self { BRelation::<L, R>::new(vec![]) }
fn _union(&self, other: &Self) -> Self { self._union(other) } fn _union(&self, other: &Self) -> Self { self._union(other) }
fn intersect(&self, other: &Self) -> Self { self.intersect(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;
}))
}
} }
...@@ -24,9 +24,12 @@ pub trait TBSet: BObject { ...@@ -24,9 +24,12 @@ pub trait TBSet: BObject {
} }
pub trait SetLike: BObject { pub trait SetLike: BObject {
type Item: BObject;
fn get_empty() -> Self; fn get_empty() -> Self;
fn _union(&self, other: &Self) -> Self; fn _union(&self, other: &Self) -> Self;
fn intersect(&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)] #[derive(Default, Debug, PartialEq, Eq, Hash, PartialOrd, Ord, Clone)]
...@@ -377,9 +380,14 @@ impl<T: 'static + BInt> BSet<T> { ...@@ -377,9 +380,14 @@ impl<T: 'static + BInt> BSet<T> {
} }
impl<T: 'static + BObject> SetLike for BSet<T> { impl<T: 'static + BObject> SetLike for BSet<T> {
type Item = T;
fn get_empty() -> Self { BSet::<T>::new(vec![]) } fn get_empty() -> Self { BSet::<T>::new(vec![]) }
fn _union(&self, other: &Self) -> Self { self._union(other) } fn _union(&self, other: &Self) -> Self { self._union(other) }
fn intersect(&self, other: &Self) -> Self { self.intersect(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> { impl<T: 'static + SetLike> BSet<T> {
......
...@@ -441,7 +441,7 @@ impl fmt::Display for <name> { ...@@ -441,7 +441,7 @@ impl fmt::Display for <name> {
>> >>
bool() ::= << bool() ::= <<
butils::BOOL (*butils::BOOL)
>> >>
include_declaration(type, identifier) ::= << include_declaration(type, identifier) ::= <<
......
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment