fix(semantics): migrate to new AST structure
This commit is contained in:
Anand Balakrishnan
parent
1c79847a77
commit
2b16ef9c40
3 changed files with 273 additions and 71 deletions
|
|
@ -1,5 +1,7 @@
|
|||
use argus_core::prelude::*;
|
||||
use argus_core::expr::*;
|
||||
use argus_core::signals::traits::{SignalAbs, TrySignalCast};
|
||||
use argus_core::signals::Signal;
|
||||
use argus_core::ArgusResult;
|
||||
use num_traits::{Num, NumCast};
|
||||
|
||||
use crate::Trace;
|
||||
|
|
@ -18,14 +20,14 @@ where
|
|||
Signal<T>: SignalAbs,
|
||||
{
|
||||
match root {
|
||||
NumExpr::IntLit(val) => Signal::constant(*val).try_cast(),
|
||||
NumExpr::UIntLit(val) => Signal::constant(*val).try_cast(),
|
||||
NumExpr::FloatLit(val) => Signal::constant(*val).try_cast(),
|
||||
NumExpr::IntVar { name } => trace.get::<i64>(name.as_str()).unwrap().try_cast(),
|
||||
NumExpr::UIntVar { name } => trace.get::<u64>(name.as_str()).unwrap().try_cast(),
|
||||
NumExpr::FloatVar { name } => trace.get::<f64>(name.as_str()).unwrap().try_cast(),
|
||||
NumExpr::Neg { arg } => eval_num_expr(arg, trace).map(|sig| -&sig),
|
||||
NumExpr::Add { args } => {
|
||||
NumExpr::IntLit(val) => Signal::constant(val.0).try_cast(),
|
||||
NumExpr::UIntLit(val) => Signal::constant(val.0).try_cast(),
|
||||
NumExpr::FloatLit(val) => Signal::constant(val.0).try_cast(),
|
||||
NumExpr::IntVar(IntVar { name }) => trace.get::<i64>(name.as_str()).unwrap().try_cast(),
|
||||
NumExpr::UIntVar(UIntVar { name }) => trace.get::<u64>(name.as_str()).unwrap().try_cast(),
|
||||
NumExpr::FloatVar(FloatVar { name }) => trace.get::<f64>(name.as_str()).unwrap().try_cast(),
|
||||
NumExpr::Neg(Neg { arg }) => eval_num_expr(arg, trace).map(|sig| -&sig),
|
||||
NumExpr::Add(Add { args }) => {
|
||||
let mut ret: Signal<T> = Signal::<T>::zero();
|
||||
for arg in args.iter() {
|
||||
let arg = eval_num_expr(arg, trace)?;
|
||||
|
|
@ -33,12 +35,12 @@ where
|
|||
}
|
||||
Ok(ret)
|
||||
}
|
||||
NumExpr::Sub { lhs, rhs } => {
|
||||
NumExpr::Sub(Sub { lhs, rhs }) => {
|
||||
let lhs = eval_num_expr(lhs, trace)?;
|
||||
let rhs = eval_num_expr(rhs, trace)?;
|
||||
Ok(&lhs - &rhs)
|
||||
}
|
||||
NumExpr::Mul { args } => {
|
||||
NumExpr::Mul(Mul { args }) => {
|
||||
let mut ret: Signal<T> = Signal::<T>::one();
|
||||
for arg in args.iter() {
|
||||
let arg = eval_num_expr(arg, trace)?;
|
||||
|
|
@ -46,12 +48,12 @@ where
|
|||
}
|
||||
Ok(ret)
|
||||
}
|
||||
NumExpr::Div { dividend, divisor } => {
|
||||
NumExpr::Div(Div { dividend, divisor }) => {
|
||||
let dividend = eval_num_expr(dividend, trace)?;
|
||||
let divisor = eval_num_expr(divisor, trace)?;
|
||||
Ok(÷nd / &divisor)
|
||||
}
|
||||
NumExpr::Abs { arg } => {
|
||||
NumExpr::Abs(Abs { arg }) => {
|
||||
let arg = eval_num_expr(arg, trace)?;
|
||||
Ok(arg.abs())
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,3 +1,7 @@
|
|||
use std::ops::Bound;
|
||||
use std::time::Duration;
|
||||
|
||||
use argus_core::expr::{Always, And, BoolVar, Cmp, Eventually, Interval, Next, Not, Or, Oracle, Until};
|
||||
use argus_core::prelude::*;
|
||||
use argus_core::signals::SignalPartialOrd;
|
||||
|
||||
|
|
@ -13,9 +17,11 @@ impl Semantics for BooleanSemantics {
|
|||
|
||||
fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output> {
|
||||
match expr {
|
||||
BoolExpr::BoolLit(val) => Ok(Signal::constant(*val)),
|
||||
BoolExpr::BoolVar { name } => trace.get(name.as_str()).cloned().ok_or(ArgusError::SignalNotPresent),
|
||||
BoolExpr::Cmp { op, lhs, rhs } => {
|
||||
BoolExpr::BoolLit(val) => Ok(Signal::constant(val.0)),
|
||||
BoolExpr::BoolVar(BoolVar { name }) => {
|
||||
trace.get(name.as_str()).cloned().ok_or(ArgusError::SignalNotPresent)
|
||||
}
|
||||
BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
|
||||
use argus_core::expr::Ordering::*;
|
||||
let lhs = eval_num_expr::<f64>(lhs, trace)?;
|
||||
let rhs = eval_num_expr::<f64>(rhs, trace)?;
|
||||
|
|
@ -29,11 +35,11 @@ impl Semantics for BooleanSemantics {
|
|||
};
|
||||
ret.ok_or(ArgusError::InvalidOperation)
|
||||
}
|
||||
BoolExpr::Not { arg } => {
|
||||
BoolExpr::Not(Not { arg }) => {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
Ok(!&arg)
|
||||
}
|
||||
BoolExpr::And { args } => {
|
||||
BoolExpr::And(And { args }) => {
|
||||
let mut ret = Signal::constant(true);
|
||||
for arg in args.iter() {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
|
|
@ -41,7 +47,7 @@ impl Semantics for BooleanSemantics {
|
|||
}
|
||||
Ok(ret)
|
||||
}
|
||||
BoolExpr::Or { args } => {
|
||||
BoolExpr::Or(Or { args }) => {
|
||||
let mut ret = Signal::constant(false);
|
||||
for arg in args.iter() {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
|
|
@ -49,46 +55,240 @@ impl Semantics for BooleanSemantics {
|
|||
}
|
||||
Ok(ret)
|
||||
}
|
||||
BoolExpr::Next { arg: _ } => todo!(),
|
||||
BoolExpr::Oracle { steps: _, arg: _ } => todo!(),
|
||||
BoolExpr::Always { arg, interval } => {
|
||||
let mut arg = Self::eval(arg, trace, ctx)?;
|
||||
match &mut arg {
|
||||
BoolExpr::Next(Next { arg }) => {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
compute_next(arg)
|
||||
}
|
||||
BoolExpr::Oracle(Oracle { steps, arg }) => {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
compute_oracle(arg, *steps)
|
||||
}
|
||||
BoolExpr::Always(Always { arg, interval }) => {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
compute_always(arg, interval)
|
||||
}
|
||||
BoolExpr::Eventually(Eventually { arg, interval }) => {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
compute_eventually(arg, interval)
|
||||
}
|
||||
BoolExpr::Until(Until { lhs, rhs, interval }) => {
|
||||
let lhs = Self::eval(lhs, trace, ctx)?;
|
||||
let rhs = Self::eval(rhs, trace, ctx)?;
|
||||
compute_until(lhs, rhs, interval)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Compute next for a signal
|
||||
fn compute_next(signal: Signal<bool>) -> ArgusResult<Signal<bool>> {
|
||||
unimplemented!()
|
||||
}
|
||||
|
||||
/// Compute oracle for a signal
|
||||
fn compute_oracle(signal: Signal<bool>, steps: usize) -> ArgusResult<Signal<bool>> {
|
||||
unimplemented!()
|
||||
}
|
||||
|
||||
/// Compute always for a signal
|
||||
fn compute_always(signal: Signal<bool>, interval: &Interval) -> ArgusResult<Signal<bool>> {
|
||||
if interval.is_empty() || interval.is_singleton() {
|
||||
return Err(ArgusError::InvalidInterval {
|
||||
reason: "interval is either empty or singleton",
|
||||
});
|
||||
}
|
||||
let ret = match signal {
|
||||
// if signal is empty or constant, return the signal itself.
|
||||
// This works because if a signal is True everythere, then it must
|
||||
// "always be true".
|
||||
Signal::Empty | Signal::Constant { value: _ } => (),
|
||||
Signal::Sampled { values, time_points } => {
|
||||
sig @ (Signal::Empty | Signal::Constant { value: _ }) => sig,
|
||||
sig => {
|
||||
use Bound::*;
|
||||
if interval.is_untimed() {
|
||||
compute_untimed_always(sig)
|
||||
} else if let (Included(a), Included(b)) = interval.into() {
|
||||
compute_timed_always(sig, *a, Some(*b))
|
||||
} else if let (Included(a), Unbounded) = interval.into() {
|
||||
compute_timed_always(sig, *a, None)
|
||||
} else {
|
||||
unreachable!("interval should be created using Interval::new, and is_untimed checks this")
|
||||
}
|
||||
}
|
||||
};
|
||||
Ok(ret)
|
||||
}
|
||||
|
||||
/// Compute timed always for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
|
||||
fn compute_timed_always(signal: Signal<bool>, a: Duration, b: Option<Duration>) -> Signal<bool> {
|
||||
match b {
|
||||
Some(b) => {
|
||||
// We want to compute the
|
||||
todo!()
|
||||
}
|
||||
None => {
|
||||
// Shift the signal to the left by `a` and then run the untimed always.
|
||||
let shifted = signal.shift_left(a);
|
||||
compute_untimed_always(shifted)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Compute untimed always
|
||||
fn compute_untimed_always(signal: Signal<bool>) -> Signal<bool> {
|
||||
let Signal::Sampled {
|
||||
mut values,
|
||||
time_points,
|
||||
} = signal
|
||||
else {
|
||||
unreachable!("we shouldn't be passing non-sampled signals here")
|
||||
};
|
||||
// Compute the & in a expanding window fashion from the back
|
||||
for i in (0..(time_points.len() - 1)).rev() {
|
||||
values[i] &= values[i + 1];
|
||||
}
|
||||
Signal::Sampled { values, time_points }
|
||||
}
|
||||
|
||||
/// Compute eventually for a signal
|
||||
fn compute_eventually(signal: Signal<bool>, interval: &Interval) -> ArgusResult<Signal<bool>> {
|
||||
if interval.is_empty() || interval.is_singleton() {
|
||||
return Err(ArgusError::InvalidInterval {
|
||||
reason: "interval is either empty or singleton",
|
||||
});
|
||||
}
|
||||
}
|
||||
Ok(arg)
|
||||
}
|
||||
BoolExpr::Eventually { arg, interval } => {
|
||||
let mut arg = Self::eval(arg, trace, ctx)?;
|
||||
match &mut arg {
|
||||
let ret = match signal {
|
||||
// if signal is empty or constant, return the signal itself.
|
||||
// This works because if a signal is True everywhere, then it must
|
||||
// "eventually be true", and if it is False everywhere, then it will
|
||||
// "never be true".
|
||||
Signal::Empty | Signal::Constant { value: _ } => (),
|
||||
Signal::Sampled { values, time_points } => {
|
||||
// This works because if a signal is True everythere, then it must
|
||||
// "eventually be true".
|
||||
sig @ (Signal::Empty | Signal::Constant { value: _ }) => sig,
|
||||
sig => {
|
||||
use Bound::*;
|
||||
if interval.is_singleton() {
|
||||
// for singleton intervals, return the signal itself.
|
||||
sig
|
||||
} else if interval.is_untimed() {
|
||||
compute_untimed_eventually(sig)
|
||||
} else if let (Included(a), Included(b)) = interval.into() {
|
||||
compute_timed_eventually(sig, *a, Some(*b))
|
||||
} else if let (Included(a), Unbounded) = interval.into() {
|
||||
compute_timed_eventually(sig, *a, None)
|
||||
} else {
|
||||
unreachable!("interval should be created using Interval::new, and is_untimed checks this")
|
||||
}
|
||||
}
|
||||
};
|
||||
Ok(ret)
|
||||
}
|
||||
|
||||
/// Compute timed eventually for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
|
||||
fn compute_timed_eventually(signal: Signal<bool>, a: Duration, b: Option<Duration>) -> Signal<bool> {
|
||||
match b {
|
||||
Some(b) => {
|
||||
// We want to compute the
|
||||
todo!()
|
||||
}
|
||||
None => {
|
||||
// Shift the signal to the left by `a` and then run the untimed eventually.
|
||||
let shifted = signal.shift_left(a);
|
||||
compute_untimed_eventually(shifted)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Compute untimed eventually
|
||||
fn compute_untimed_eventually(signal: Signal<bool>) -> Signal<bool> {
|
||||
let Signal::Sampled {
|
||||
mut values,
|
||||
time_points,
|
||||
} = signal
|
||||
else {
|
||||
unreachable!("we shouldn't be passing non-sampled signals here")
|
||||
};
|
||||
// Compute the | in a expanding window fashion from the back
|
||||
for i in (0..(time_points.len() - 1)).rev() {
|
||||
values[i] |= values[i + 1];
|
||||
}
|
||||
Signal::Sampled { values, time_points }
|
||||
}
|
||||
|
||||
/// Compute until
|
||||
fn compute_until(lhs: Signal<bool>, rhs: Signal<bool>, interval: &Interval) -> ArgusResult<Signal<bool>> {
|
||||
let ret = match (lhs, rhs) {
|
||||
// If either signals are empty, return empty
|
||||
(sig @ Signal::Empty, _) | (_, sig @ Signal::Empty) => sig,
|
||||
(_, Signal::Constant { value: false }) => Signal::const_false(),
|
||||
(_, Signal::Constant { value: true }) => Signal::const_true(),
|
||||
|
||||
(Signal::Constant { value: true }, sig) => {
|
||||
// This is the identity for eventually
|
||||
compute_eventually(sig, interval)?
|
||||
}
|
||||
(Signal::Constant { value: false }, sig) => {
|
||||
// This is the identity for next
|
||||
compute_next(sig)?
|
||||
}
|
||||
(
|
||||
lhs @ Signal::Sampled {
|
||||
values: _,
|
||||
time_points: _,
|
||||
},
|
||||
rhs @ Signal::Sampled {
|
||||
values: _,
|
||||
time_points: _,
|
||||
},
|
||||
) => {
|
||||
use Bound::*;
|
||||
if interval.is_untimed() {
|
||||
compute_untimed_until(lhs, rhs)
|
||||
} else if let (Included(a), Included(b)) = interval.into() {
|
||||
compute_timed_until(lhs, rhs, *a, Some(*b))
|
||||
} else if let (Included(a), Unbounded) = interval.into() {
|
||||
compute_timed_until(lhs, rhs, *a, None)
|
||||
} else {
|
||||
unreachable!("interval should be created using Interval::new, and is_untimed checks this")
|
||||
}
|
||||
}
|
||||
Ok(arg)
|
||||
};
|
||||
Ok(ret)
|
||||
}
|
||||
|
||||
/// Compute timed until for the interval `[a, b]` (or, if `b` is `None`, `[a, ..]`.
|
||||
fn compute_timed_until(lhs: Signal<bool>, rhs: Signal<bool>, a: Duration, b: Option<Duration>) -> Signal<bool> {
|
||||
// For this, we will perform the Until rewrite defined in [1]:
|
||||
//
|
||||
// $$
|
||||
// \varphi_1 U_{[a, b]} \varphi_2 = F_{[a,b]} \varphi_2 \land (\varphi_1 U_{[a,
|
||||
// \infty)} \varphi_2)
|
||||
// $$
|
||||
//
|
||||
// $$
|
||||
// \varphi_1 U_{[a, \infty)} \varphi_2 = G_{[0,a]} (\varphi_1 U \varphi_2)
|
||||
// $$
|
||||
//
|
||||
//
|
||||
// [1] A. Donzé, T. Ferrère, and O. Maler, "Efficient Robust Monitoring for STL." doi:
|
||||
// 10.1007/978-3-642-39799-8_19.
|
||||
|
||||
match b {
|
||||
Some(b) => {
|
||||
// First compute eventually [a, b]
|
||||
let ev_a_b_rhs = compute_timed_eventually(rhs, a, Some(b));
|
||||
// Then compute until [a, \infty) (lhs, rhs)
|
||||
let unt_a_inf = compute_timed_until(lhs, rhs, a, None);
|
||||
// Then & them
|
||||
&ev_a_b_rhs & &unt_a_inf
|
||||
}
|
||||
BoolExpr::Until {
|
||||
lhs: _,
|
||||
rhs: _,
|
||||
interval,
|
||||
} => todo!(),
|
||||
None => {
|
||||
// First compute untimed until (lhs, rhs)
|
||||
let untimed_until = compute_untimed_until(lhs, rhs);
|
||||
// Compute G [0, a]
|
||||
compute_untimed_always(untimed_until)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// Compute untimed until
|
||||
fn compute_untimed_until(lhs: Signal<bool>, rhs: Signal<bool>) -> Signal<bool> {
|
||||
let sync_points = lhs.sync_with_intersection(&rhs);
|
||||
todo!()
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
use std::iter::zip;
|
||||
|
||||
use argus_core::expr::BoolExpr;
|
||||
use argus_core::expr::{Always, And, BoolExpr, BoolVar, Cmp, Eventually, Next, Not, Or, Oracle, Until};
|
||||
use argus_core::prelude::*;
|
||||
use argus_core::signals::traits::{SignalAbs, SignalMinMax};
|
||||
use argus_core::signals::SignalNumCast;
|
||||
|
|
@ -27,12 +27,12 @@ impl Semantics for QuantitativeSemantics {
|
|||
|
||||
fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output> {
|
||||
let ret: Self::Output = match expr {
|
||||
BoolExpr::BoolLit(val) => top_or_bot(&Signal::constant(*val)),
|
||||
BoolExpr::BoolVar { name } => {
|
||||
BoolExpr::BoolLit(val) => top_or_bot(&Signal::constant(val.0)),
|
||||
BoolExpr::BoolVar(BoolVar { name }) => {
|
||||
let sig = trace.get::<bool>(name.as_str()).ok_or(ArgusError::SignalNotPresent)?;
|
||||
top_or_bot(sig)
|
||||
}
|
||||
BoolExpr::Cmp { op, lhs, rhs } => {
|
||||
BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
|
||||
use argus_core::expr::Ordering::*;
|
||||
let lhs = eval_num_expr::<f64>(lhs, trace)?;
|
||||
let rhs = eval_num_expr::<f64>(rhs, trace)?;
|
||||
|
|
@ -44,11 +44,11 @@ impl Semantics for QuantitativeSemantics {
|
|||
Greater { strict: _ } => &lhs - &rhs,
|
||||
}
|
||||
}
|
||||
BoolExpr::Not { arg } => {
|
||||
BoolExpr::Not(Not { arg }) => {
|
||||
let arg = Self::eval(arg, trace, ctx)?;
|
||||
-&arg
|
||||
}
|
||||
BoolExpr::And { args } => {
|
||||
BoolExpr::And(And { args }) => {
|
||||
assert!(args.len() >= 2);
|
||||
let args = args
|
||||
.iter()
|
||||
|
|
@ -58,7 +58,7 @@ impl Semantics for QuantitativeSemantics {
|
|||
.reduce(|lhs, rhs| lhs.min(&rhs))
|
||||
.ok_or(ArgusError::InvalidOperation)?
|
||||
}
|
||||
BoolExpr::Or { args } => {
|
||||
BoolExpr::Or(Or { args }) => {
|
||||
assert!(args.len() >= 2);
|
||||
let args = args
|
||||
.iter()
|
||||
|
|
@ -68,9 +68,9 @@ impl Semantics for QuantitativeSemantics {
|
|||
.reduce(|lhs, rhs| lhs.max(&rhs))
|
||||
.ok_or(ArgusError::InvalidOperation)?
|
||||
}
|
||||
BoolExpr::Next { arg: _ } => todo!(),
|
||||
BoolExpr::Oracle { steps: _, arg: _ } => todo!(),
|
||||
BoolExpr::Always { arg, interval } => {
|
||||
BoolExpr::Next(Next { arg: _ }) => todo!(),
|
||||
BoolExpr::Oracle(Oracle { steps: _, arg: _ }) => todo!(),
|
||||
BoolExpr::Always(Always { arg, interval: _ }) => {
|
||||
let mut arg = Self::eval(arg, trace, ctx)?;
|
||||
match &mut arg {
|
||||
// if signal is empty or constant, return the signal itself.
|
||||
|
|
@ -86,7 +86,7 @@ impl Semantics for QuantitativeSemantics {
|
|||
}
|
||||
arg
|
||||
}
|
||||
BoolExpr::Eventually { arg, interval } => {
|
||||
BoolExpr::Eventually(Eventually { arg, interval: _ }) => {
|
||||
let mut arg = Self::eval(arg, trace, ctx)?;
|
||||
match &mut arg {
|
||||
// if signal is empty or constant, return the signal itself.
|
||||
|
|
@ -102,11 +102,11 @@ impl Semantics for QuantitativeSemantics {
|
|||
}
|
||||
arg
|
||||
}
|
||||
BoolExpr::Until {
|
||||
BoolExpr::Until(Until {
|
||||
lhs: _,
|
||||
rhs: _,
|
||||
interval,
|
||||
} => todo!(),
|
||||
interval: _,
|
||||
}) => todo!(),
|
||||
};
|
||||
Ok(ret)
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue