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

feat(argus-semantics): complete boolean semantics

Browse source
This commit is contained in:
Anand Balakrishnan 2023-08-30 12:46:52 -07:00
parent ad9afb4eba
commit c916db3853
No known key found for this signature in database
6 changed files with 149 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

1
argus-semantics/src/eval.rs
View file

@ -0,0 +1 @@

1
argus-semantics/src/lib.rs
View file

@ -8,4 +8,5 @@ pub mod semantics;
pub mod traits;
pub mod utils;
pub use semantics::{BooleanSemantics, QuantitativeSemantics};
pub use traits::Trace;

77
argus-semantics/src/semantics/boolean.rs
View file

@ -124,9 +124,28 @@ fn compute_always(signal: Signal<bool>, interval: &Interval) -> ArgusResult<Sign
reason: "interval is either empty or singleton",
});
}
let z1 = !signal;
let z2 = compute_eventually(z1, interval)?;
Ok(!z2)
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".
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_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, ..]`.
@ -147,7 +166,7 @@ fn compute_untimed_always(signal: Signal<bool>) -> ArgusResult<Signal<bool>> {
};
// Compute the & in a expanding window fashion from the back
for i in (0..(time_points.len() - 1)).rev() {
values[i] &= values[i + 1];
values[i] = values[i + 1].min(values[i]);
}
Ok(Signal::Sampled { values, time_points })
}
@ -237,7 +256,7 @@ fn compute_untimed_eventually(signal: Signal<bool>) -> ArgusResult<Signal<bool>>
};
// Compute the | in a expanding window fashion from the back
for i in (0..(time_points.len() - 1)).rev() {
values[i] |= values[i + 1];
values[i] = values[i + 1].max(values[i]);
}
Ok(Signal::Sampled { values, time_points })
}
@ -247,27 +266,7 @@ fn compute_until(lhs: Signal<bool>, rhs: Signal<bool>, interval: &Interval) -> A
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: _,
},
) => {
(lhs, rhs) => {
use Bound::*;
if interval.is_untimed() {
compute_untimed_until(lhs, rhs)?
@ -309,21 +308,39 @@ fn compute_timed_until(
// Then compute until [a, \infty) (lhs, rhs)
let unt_a_inf = compute_timed_until(lhs, rhs, a, None)?;
// Then & them
Ok(&ev_a_b_rhs & &unt_a_inf)
Ok(ev_a_b_rhs.min(&unt_a_inf))
}
None => {
assert_ne!(a, Duration::ZERO, "untimed case wasn't handled for Until");
// First compute untimed until (lhs, rhs)
let untimed_until = compute_untimed_until(lhs, rhs)?;
// Compute G [0, a]
compute_untimed_always(untimed_until)
compute_timed_always(untimed_until, Duration::ZERO, Some(a))
}
}
}
/// Compute untimed until
fn compute_untimed_until(lhs: Signal<bool>, rhs: Signal<bool>) -> ArgusResult<Signal<bool>> {
let sync_points = lhs.sync_with_intersection::<Linear>(&rhs);
todo!()
let sync_points = lhs.sync_with_intersection::<Linear>(&rhs).unwrap();
let mut ret_samples = Vec::with_capacity(sync_points.len());
let expected_len = sync_points.len();
let mut next = false;
for (i, t) in sync_points.into_iter().enumerate().rev() {
let v1 = lhs.interpolate_at::<Linear>(t).unwrap();
let v2 = rhs.interpolate_at::<Linear>(t).unwrap();
let z = (v1 && v2) || (v1 && next);
if z == next && i < (expected_len - 2) {
ret_samples.pop();
}
ret_samples.push((t, z));
next = z;
}
Signal::<bool>::try_from_iter(ret_samples.into_iter().rev())
}
#[cfg(test)]

72
argus-semantics/src/semantics/quantitative.rs
View file

@ -567,7 +567,7 @@ mod tests {
let trace = MyTrace { signals };
let rob = dbg!(QuantitativeSemantics::eval(&spec, &trace).unwrap());
let rob = QuantitativeSemantics::eval(&spec, &trace).unwrap();
let expected = Signal::from_iter(vec![
(Duration::from_secs_f64(0.0), 0.0 - 1.3),
(Duration::from_secs_f64(0.7), 0.0 - 3.0),
@ -613,4 +613,74 @@ mod tests {
assert_equal(&rob, &expected);
}
}
#[test]
fn unbounded_until() {
let mut ctx = ExprBuilder::new();
let a = ctx.int_var("a".to_owned()).unwrap();
let b = ctx.int_var("b".to_owned()).unwrap();
let lhs = ctx.make_gt(a, ctx.int_const(0));
let rhs = ctx.make_gt(b, ctx.int_const(0));
let spec = ctx.make_until(lhs, rhs);
{
let signals = HashMap::from_iter(vec![
(
"a".to_owned(),
Box::new(Signal::<i64>::from_iter(vec![
(Duration::from_secs(0), 2),
(Duration::from_secs(5), 2),
])) as Box<dyn AnySignal>,
),
(
"b".to_owned(),
Box::new(Signal::<i64>::from_iter(vec![
(Duration::from_secs(0), 4),
(Duration::from_secs(5), 4),
])) as Box<dyn AnySignal>,
),
]);
let trace = MyTrace { signals };
let rob = QuantitativeSemantics::eval(&spec, &trace).unwrap();
let expected = Signal::from_iter(vec![(Duration::from_secs(0), 2), (Duration::from_secs(5), 2)])
.num_cast::<f64>()
.unwrap();
assert_equal(&rob, &expected);
}
{
let signals = HashMap::from_iter(vec![
(
"a".to_owned(),
Box::new(Signal::<i64>::from_iter(vec![
(Duration::from_secs_f64(1.0), 1),
(Duration::from_secs_f64(3.5), 7),
(Duration::from_secs_f64(4.7), 3),
(Duration::from_secs_f64(5.3), 5),
(Duration::from_secs_f64(6.2), 1),
])) as Box<dyn AnySignal>,
),
(
"b".to_owned(),
Box::new(Signal::<i64>::from_iter(vec![
(Duration::from_secs(4), 2),
(Duration::from_secs(6), 3),
])) as Box<dyn AnySignal>,
),
]);
let trace = MyTrace { signals };
let rob = QuantitativeSemantics::eval(&spec, &trace).unwrap();
let expected = Signal::from_iter(vec![(Duration::from_secs(4), 3), (Duration::from_secs(6), 3)])
.num_cast::<f64>()
.unwrap();
assert_equal(&rob, &expected);
}
}
}