diff --git a/argus-semantics/src/semantics/boolean.rs b/argus-semantics/src/semantics/boolean.rs index 294db63..ed7e724 100644 --- a/argus-semantics/src/semantics/boolean.rs +++ b/argus-semantics/src/semantics/boolean.rs @@ -50,7 +50,8 @@ impl Semantics for BooleanSemantics { Ok(ret) } BoolExpr::Next { arg: _ } => todo!(), - BoolExpr::Always { arg } => { + BoolExpr::Oracle { steps: _, arg: _ } => todo!(), + BoolExpr::Always { arg, interval } => { let mut arg = Self::eval(arg, trace, ctx)?; match &mut arg { // if signal is empty or constant, return the signal itself. @@ -66,7 +67,7 @@ impl Semantics for BooleanSemantics { } Ok(arg) } - BoolExpr::Eventually { arg } => { + BoolExpr::Eventually { arg, interval } => { let mut arg = Self::eval(arg, trace, ctx)?; match &mut arg { // if signal is empty or constant, return the signal itself. @@ -83,7 +84,11 @@ impl Semantics for BooleanSemantics { } Ok(arg) } - BoolExpr::Until { lhs: _, rhs: _ } => todo!(), + BoolExpr::Until { + lhs: _, + rhs: _, + interval, + } => todo!(), } } } diff --git a/argus-semantics/src/semantics/quantitative.rs b/argus-semantics/src/semantics/quantitative.rs index c83ae54..52a05dc 100644 --- a/argus-semantics/src/semantics/quantitative.rs +++ b/argus-semantics/src/semantics/quantitative.rs @@ -69,7 +69,8 @@ impl Semantics for QuantitativeSemantics { .ok_or(ArgusError::InvalidOperation)? } BoolExpr::Next { arg: _ } => todo!(), - BoolExpr::Always { arg } => { + BoolExpr::Oracle { steps: _, arg: _ } => todo!(), + BoolExpr::Always { arg, interval } => { let mut arg = Self::eval(arg, trace, ctx)?; match &mut arg { // if signal is empty or constant, return the signal itself. @@ -85,7 +86,7 @@ impl Semantics for QuantitativeSemantics { } arg } - BoolExpr::Eventually { arg } => { + BoolExpr::Eventually { arg, interval } => { let mut arg = Self::eval(arg, trace, ctx)?; match &mut arg { // if signal is empty or constant, return the signal itself. @@ -101,7 +102,11 @@ impl Semantics for QuantitativeSemantics { } arg } - BoolExpr::Until { lhs: _, rhs: _ } => todo!(), + BoolExpr::Until { + lhs: _, + rhs: _, + interval, + } => todo!(), }; Ok(ret) }