research/argus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(core): add LTL temporal expressions

Browse source
This commit is contained in:
Anand Balakrishnan 2023-04-07 14:05:35 -07:00
parent c322d34859
commit a6a3805107
No known key found for this signature in database
1 changed files with 22 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

23
argus-core/src/expr.rs
View file

@ -104,6 +104,11 @@ pub enum BoolExpr {
Not { arg: Box<BoolExpr> },
And { args: Vec<BoolExpr> },
Or { args: Vec<BoolExpr> },
Next { arg: Box<BoolExpr> },
Always { arg: Box<BoolExpr> },
Eventually { arg: Box<BoolExpr> },
Until { lhs: Box<BoolExpr>, rhs: Box<BoolExpr> },
}
impl Expr for BoolExpr {
@ -291,6 +296,18 @@ impl ExprBuilder {
Ok(Box::new(BoolExpr::And { args }))
}
}
pub fn make_next(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
Box::new(BoolExpr::Next { arg })
}
pub fn make_always(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
Box::new(BoolExpr::Always { arg })
}
pub fn make_eventually(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
Box::new(BoolExpr::Eventually { arg })
}
}
#[cfg(any(test, feature = "arbitrary"))]
@ -362,11 +379,15 @@ pub mod arbitrary {
args: args.into_iter().map(|arg| *arg).collect(),
})
}),
prop::collection::vec(inner, 0..10).prop_map(|args| {
prop::collection::vec(inner.clone(), 0..10).prop_map(|args| {
Box::new(BoolExpr::Or {
args: args.into_iter().map(|arg| *arg).collect(),
})
}),
inner.clone().prop_map(|arg| Box::new(BoolExpr::Next { arg })),
inner.clone().prop_map(|arg| Box::new(BoolExpr::Always { arg })),
inner.clone().prop_map(|arg| Box::new(BoolExpr::Eventually { arg })),
(inner.clone(), inner).prop_map(|(lhs, rhs)| Box::new(BoolExpr::Until { lhs, rhs })),
]
},
)