refactor!(argus): combine co-dependent crates
- argus-core, argus-parser, argus-semantics are highly co-dependent, and hence should be in the same create.
This commit is contained in:
parent
dc71a51df3
commit
7ce056b471
43 changed files with 281 additions and 399 deletions
10
Cargo.toml
10
Cargo.toml
|
|
@ -1,13 +1,5 @@
|
||||||
[workspace]
|
[workspace]
|
||||||
members = [
|
members = ["argus", "argus-derive", "argus-automata", "pyargus"]
|
||||||
"argus",
|
|
||||||
"argus-core",
|
|
||||||
"argus-semantics",
|
|
||||||
"argus-derive",
|
|
||||||
"argus-parser",
|
|
||||||
"argus-automata",
|
|
||||||
"pyargus",
|
|
||||||
]
|
|
||||||
|
|
||||||
resolver = "2"
|
resolver = "2"
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,27 +0,0 @@
|
||||||
[package]
|
|
||||||
name = "argus-core"
|
|
||||||
version = "0.1.1"
|
|
||||||
|
|
||||||
authors.workspace = true
|
|
||||||
license.workspace = true
|
|
||||||
edition.workspace = true
|
|
||||||
rust-version.workspace = true
|
|
||||||
readme.workspace = true
|
|
||||||
repository.workspace = true
|
|
||||||
|
|
||||||
[dependencies]
|
|
||||||
derive_more = "0.99.17"
|
|
||||||
itertools = "0.11"
|
|
||||||
paste = "1.0.14"
|
|
||||||
num-traits = "0.2.16"
|
|
||||||
thiserror = "1.0.47"
|
|
||||||
proptest = { version = "1.2", optional = true }
|
|
||||||
enum_dispatch = "0.3.12"
|
|
||||||
argus-derive = { version = "0.1.0", path = "../argus-derive" }
|
|
||||||
|
|
||||||
[dev-dependencies]
|
|
||||||
argus-core = { path = ".", features = ["arbitrary"] }
|
|
||||||
|
|
||||||
[features]
|
|
||||||
default = []
|
|
||||||
arbitrary = ["dep:proptest"]
|
|
||||||
|
|
@ -1,23 +0,0 @@
|
||||||
use enum_dispatch::enum_dispatch;
|
|
||||||
|
|
||||||
use super::{BoolExpr, ExprRef, NumExpr};
|
|
||||||
|
|
||||||
/// A trait representing expressions
|
|
||||||
#[enum_dispatch]
|
|
||||||
pub trait AnyExpr {
|
|
||||||
/// Check if the given expression is a numeric expression
|
|
||||||
fn is_numeric(&self) -> bool;
|
|
||||||
/// Check if the given expression is a boolean expression
|
|
||||||
fn is_boolean(&self) -> bool;
|
|
||||||
/// Get the arguments to the current expression.
|
|
||||||
///
|
|
||||||
/// If the expression doesn't contain arguments (i.e., it is a leaf expression) then
|
|
||||||
/// the vector is empty.
|
|
||||||
fn args(&self) -> Vec<ExprRef<'_>>;
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Marker trait for numeric expressions
|
|
||||||
pub trait IsNumExpr: AnyExpr + Into<NumExpr> {}
|
|
||||||
|
|
||||||
/// Marker trait for Boolean expressions
|
|
||||||
pub trait IsBoolExpr: AnyExpr + Into<BoolExpr> {}
|
|
||||||
|
|
@ -1,104 +0,0 @@
|
||||||
//! # `argus-core`
|
|
||||||
//!
|
|
||||||
//! This crate provides some of the core functionality or interfaces for the other Argus
|
|
||||||
//! components. Mainly, the crate provides:
|
|
||||||
//!
|
|
||||||
//! 1. Expression tree nodes for defining temporal logic specifications (see [`expr`]).
|
|
||||||
//! 2. Different signal types for generating traces of data (see [`signals`]).
|
|
||||||
//! 3. A list of possible errors any component in Argus can generate (see
|
|
||||||
//! [`enum@Error`]).
|
|
||||||
|
|
||||||
#![warn(missing_docs)]
|
|
||||||
extern crate self as argus_core;
|
|
||||||
|
|
||||||
pub mod expr;
|
|
||||||
pub mod prelude;
|
|
||||||
pub mod signals;
|
|
||||||
|
|
||||||
use std::time::Duration;
|
|
||||||
|
|
||||||
pub use expr::*;
|
|
||||||
pub use signals::Signal;
|
|
||||||
use thiserror::Error;
|
|
||||||
|
|
||||||
/// Errors generated by all Argus components.
|
|
||||||
#[derive(Error, Debug)]
|
|
||||||
pub enum Error {
|
|
||||||
/// An identifier has been redeclared in a specification.
|
|
||||||
///
|
|
||||||
/// This is called mainly from [`expr::ExprBuilder`].
|
|
||||||
#[error("redeclaration of identifier")]
|
|
||||||
IdentifierRedeclaration,
|
|
||||||
|
|
||||||
/// An expression is provided with an insufficient number of arguments.
|
|
||||||
///
|
|
||||||
/// This is called for N-ary expressions:
|
|
||||||
/// [`NumExpr::Add`](crate::expr::NumExpr::Add),
|
|
||||||
/// [`NumExpr::Mul`](crate::expr::NumExpr::Mul),
|
|
||||||
/// [`BoolExpr::And`](crate::expr::BoolExpr::And), and
|
|
||||||
/// [`BoolExpr::Or`](crate::expr::BoolExpr::Or).
|
|
||||||
#[error("insufficient number of arguments")]
|
|
||||||
IncompleteArgs,
|
|
||||||
|
|
||||||
/// Attempting to `push` a new sample to a non-sampled signal
|
|
||||||
/// ([`Signal::Empty`](crate::signals::Signal::Empty) or
|
|
||||||
/// [`Signal::Constant`](crate::signals::Signal::Constant)).
|
|
||||||
#[error("cannot push value to non-sampled signal")]
|
|
||||||
InvalidPushToSignal,
|
|
||||||
|
|
||||||
/// Pushing the new value to the sampled signal makes it not strictly monotonically
|
|
||||||
/// increasing.
|
|
||||||
#[error(
|
|
||||||
"trying to create a non-monotonically signal, signal end time ({end_time:?}) > sample time point \
|
|
||||||
({current_sample:?})"
|
|
||||||
)]
|
|
||||||
NonMonotonicSignal {
|
|
||||||
/// The time that the signal actually ends
|
|
||||||
end_time: Duration,
|
|
||||||
/// The time point of the new (erroneous) sample.
|
|
||||||
current_sample: Duration,
|
|
||||||
},
|
|
||||||
|
|
||||||
/// Attempting to perform an invalid operation on a signal
|
|
||||||
#[error("invalid operation on signal")]
|
|
||||||
InvalidOperation,
|
|
||||||
|
|
||||||
/// Attempting to index a signal not present in a trace.
|
|
||||||
#[error("name not in signal trace")]
|
|
||||||
SignalNotPresent,
|
|
||||||
|
|
||||||
/// Attempting to perform a signal operation not supported by the type
|
|
||||||
#[error("incorrect signal type")]
|
|
||||||
InvalidSignalType,
|
|
||||||
|
|
||||||
/// Incorrect cast of signal
|
|
||||||
#[error("invalid cast from {from} to {to}")]
|
|
||||||
InvalidCast {
|
|
||||||
/// Type of the signal being cast from
|
|
||||||
from: &'static str,
|
|
||||||
/// Type of the signal being cast to
|
|
||||||
to: &'static str,
|
|
||||||
},
|
|
||||||
|
|
||||||
/// Invalid interval
|
|
||||||
#[error("invalid interval: {reason}")]
|
|
||||||
InvalidInterval {
|
|
||||||
/// Reason for interval being invalid
|
|
||||||
reason: &'static str,
|
|
||||||
},
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Error {
|
|
||||||
/// An [`InvalidCast`](Error::InvalidCast) error from `T` to `U`.
|
|
||||||
pub fn invalid_cast<T, U>() -> Self {
|
|
||||||
Self::InvalidCast {
|
|
||||||
from: std::any::type_name::<T>(),
|
|
||||||
to: std::any::type_name::<U>(),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Alias for [`Error`](enum@Error)
|
|
||||||
pub type ArgusError = Error;
|
|
||||||
/// Alias for [`Result<T, ArgusError>`]
|
|
||||||
pub type ArgusResult<T> = Result<T, Error>;
|
|
||||||
|
|
@ -1,5 +0,0 @@
|
||||||
#![doc(hidden)]
|
|
||||||
|
|
||||||
pub use crate::expr::*;
|
|
||||||
pub use crate::signals::Signal;
|
|
||||||
pub use crate::{ArgusError, ArgusResult};
|
|
||||||
|
|
@ -3,12 +3,12 @@ use proc_macro2::{Ident, Span};
|
||||||
use quote::{quote, ToTokens};
|
use quote::{quote, ToTokens};
|
||||||
use syn::DeriveInput;
|
use syn::DeriveInput;
|
||||||
|
|
||||||
/// Implement [`IsBoolExpr`](argus_core::expr::traits::IsBoolExpr) and other Boolean
|
/// Implement [`IsBoolExpr`](argus::expr::IsBoolExpr) and other Boolean
|
||||||
/// operations (`Not`, `BitOr`, and `BitAnd`) for the input identifier.
|
/// operations (`Not`, `BitOr`, and `BitAnd`) for the input identifier.
|
||||||
pub fn bool_expr_impl(input: DeriveInput) -> TokenStream {
|
pub fn bool_expr_impl(input: DeriveInput) -> TokenStream {
|
||||||
let ident = &input.ident;
|
let ident = &input.ident;
|
||||||
let marker_impl = quote! {
|
let marker_impl = quote! {
|
||||||
impl ::argus_core::expr::traits::IsBoolExpr for #ident {}
|
impl ::argus::expr::IsBoolExpr for #ident {}
|
||||||
};
|
};
|
||||||
|
|
||||||
let not_impl = impl_bool_not(&input);
|
let not_impl = impl_bool_not(&input);
|
||||||
|
|
@ -29,11 +29,11 @@ fn impl_bool_not(input: &DeriveInput) -> impl ToTokens {
|
||||||
let ident = &input.ident;
|
let ident = &input.ident;
|
||||||
quote! {
|
quote! {
|
||||||
impl ::core::ops::Not for #ident {
|
impl ::core::ops::Not for #ident {
|
||||||
type Output = ::argus_core::expr::BoolExpr;
|
type Output = ::argus::expr::BoolExpr;
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
fn not(self) -> Self::Output {
|
fn not(self) -> Self::Output {
|
||||||
(::argus_core::expr::Not { arg: Box::new(self.into()) }).into()
|
(::argus::expr::Not { arg: Box::new(self.into()) }).into()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -62,12 +62,12 @@ fn impl_bool_and_or(input: &DeriveInput, op: BoolOp) -> impl ToTokens {
|
||||||
};
|
};
|
||||||
quote! {
|
quote! {
|
||||||
impl ::core::ops::#trait_name for #ident {
|
impl ::core::ops::#trait_name for #ident {
|
||||||
type Output = ::argus_core::expr::BoolExpr;
|
type Output = ::argus::expr::BoolExpr;
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
fn #trait_fn(self, other: Self) -> Self::Output {
|
fn #trait_fn(self, other: Self) -> Self::Output {
|
||||||
use ::argus_core::expr::BoolExpr;
|
use ::argus::expr::BoolExpr;
|
||||||
use ::argus_core::expr::#enum_id;
|
use ::argus::expr::#enum_id;
|
||||||
let lhs: BoolExpr = self.into();
|
let lhs: BoolExpr = self.into();
|
||||||
let rhs: BoolExpr = other.into();
|
let rhs: BoolExpr = other.into();
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -3,12 +3,12 @@ use proc_macro2::{Ident, Span};
|
||||||
use quote::{quote, ToTokens};
|
use quote::{quote, ToTokens};
|
||||||
use syn::DeriveInput;
|
use syn::DeriveInput;
|
||||||
|
|
||||||
/// Implement [`IsNumExpr`](argus_core::expr::traits::IsNumExpr) and other Numean
|
/// Implement [`IsNumExpr`](argus::expr::IsNumExpr) and other Numean
|
||||||
/// operations (`Neg`, `Add`, `Mul`, `Sub`, and `Div`) for the input identifier.
|
/// operations (`Neg`, `Add`, `Mul`, `Sub`, and `Div`) for the input identifier.
|
||||||
pub fn num_expr_impl(input: DeriveInput) -> TokenStream {
|
pub fn num_expr_impl(input: DeriveInput) -> TokenStream {
|
||||||
let ident = &input.ident;
|
let ident = &input.ident;
|
||||||
let marker_impl = quote! {
|
let marker_impl = quote! {
|
||||||
impl ::argus_core::expr::traits::IsNumExpr for #ident {}
|
impl ::argus::expr::IsNumExpr for #ident {}
|
||||||
};
|
};
|
||||||
|
|
||||||
let neg_impl = impl_num_neg(&input);
|
let neg_impl = impl_num_neg(&input);
|
||||||
|
|
@ -33,11 +33,11 @@ fn impl_num_neg(input: &DeriveInput) -> impl ToTokens {
|
||||||
let ident = &input.ident;
|
let ident = &input.ident;
|
||||||
quote! {
|
quote! {
|
||||||
impl ::core::ops::Neg for #ident {
|
impl ::core::ops::Neg for #ident {
|
||||||
type Output = ::argus_core::expr::NumExpr;
|
type Output = ::argus::expr::NumExpr;
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
fn neg(self) -> Self::Output {
|
fn neg(self) -> Self::Output {
|
||||||
(::argus_core::expr::Neg { arg: Box::new(self.into()) }).into()
|
(::argus::expr::Neg { arg: Box::new(self.into()) }).into()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -79,14 +79,14 @@ fn impl_nary_op(input: &DeriveInput, op: NumOp) -> impl ToTokens {
|
||||||
quote! {
|
quote! {
|
||||||
impl<T> ::core::ops::#trait_name<T> for #ident
|
impl<T> ::core::ops::#trait_name<T> for #ident
|
||||||
where
|
where
|
||||||
T: ::core::convert::Into<::argus_core::expr::NumExpr>
|
T: ::core::convert::Into<::argus::expr::NumExpr>
|
||||||
{
|
{
|
||||||
type Output = ::argus_core::expr::NumExpr;
|
type Output = ::argus::expr::NumExpr;
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
fn #trait_fn(self, other: T) -> Self::Output {
|
fn #trait_fn(self, other: T) -> Self::Output {
|
||||||
use ::argus_core::expr::NumExpr;
|
use ::argus::expr::NumExpr;
|
||||||
use ::argus_core::expr::#node_name;
|
use ::argus::expr::#node_name;
|
||||||
let lhs: NumExpr = self.into();
|
let lhs: NumExpr = self.into();
|
||||||
let rhs: NumExpr = other.into();
|
let rhs: NumExpr = other.into();
|
||||||
|
|
||||||
|
|
@ -115,13 +115,13 @@ fn impl_sub(input: &DeriveInput) -> impl ToTokens {
|
||||||
quote! {
|
quote! {
|
||||||
impl<T> ::core::ops::Sub<T> for #ident
|
impl<T> ::core::ops::Sub<T> for #ident
|
||||||
where
|
where
|
||||||
T: ::core::convert::Into<::argus_core::expr::NumExpr>
|
T: ::core::convert::Into<::argus::expr::NumExpr>
|
||||||
{
|
{
|
||||||
type Output = ::argus_core::expr::NumExpr;
|
type Output = ::argus::expr::NumExpr;
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
fn sub(self, other: T) -> Self::Output {
|
fn sub(self, other: T) -> Self::Output {
|
||||||
use ::argus_core::expr::Sub;
|
use ::argus::expr::Sub;
|
||||||
let expr = Sub {
|
let expr = Sub {
|
||||||
lhs: Box::new(self.into()),
|
lhs: Box::new(self.into()),
|
||||||
rhs: Box::new(other.into())
|
rhs: Box::new(other.into())
|
||||||
|
|
@ -137,13 +137,13 @@ fn impl_div(input: &DeriveInput) -> impl ToTokens {
|
||||||
quote! {
|
quote! {
|
||||||
impl<T> ::core::ops::Div<T> for #ident
|
impl<T> ::core::ops::Div<T> for #ident
|
||||||
where
|
where
|
||||||
T: ::core::convert::Into<::argus_core::expr::NumExpr>
|
T: ::core::convert::Into<::argus::expr::NumExpr>
|
||||||
{
|
{
|
||||||
type Output = ::argus_core::expr::NumExpr;
|
type Output = ::argus::expr::NumExpr;
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
fn div(self, other: T) -> Self::Output {
|
fn div(self, other: T) -> Self::Output {
|
||||||
use ::argus_core::expr::Div;
|
use ::argus::expr::Div;
|
||||||
let expr = Div {
|
let expr = Div {
|
||||||
dividend: Box::new(self.into()),
|
dividend: Box::new(self.into()),
|
||||||
divisor: Box::new(other.into())
|
divisor: Box::new(other.into())
|
||||||
|
|
|
||||||
|
|
@ -1,27 +0,0 @@
|
||||||
[package]
|
|
||||||
name = "argus-parser"
|
|
||||||
version = "0.1.1"
|
|
||||||
|
|
||||||
authors.workspace = true
|
|
||||||
license.workspace = true
|
|
||||||
edition.workspace = true
|
|
||||||
rust-version.workspace = true
|
|
||||||
readme.workspace = true
|
|
||||||
repository.workspace = true
|
|
||||||
|
|
||||||
[[example]]
|
|
||||||
name = "dump_parse_tree"
|
|
||||||
required-features = ["reporting"]
|
|
||||||
|
|
||||||
[[example]]
|
|
||||||
name = "dump_expr"
|
|
||||||
required-features = ["reporting"]
|
|
||||||
|
|
||||||
[dependencies]
|
|
||||||
argus-core = { version = "0.1.1", path = "../argus-core" }
|
|
||||||
ariadne = { version = "0.3.0", optional = true }
|
|
||||||
chumsky = { version = "1.0.0-alpha.4", features = ["default", "label"] }
|
|
||||||
|
|
||||||
[features]
|
|
||||||
default = []
|
|
||||||
reporting = ["dep:ariadne"]
|
|
||||||
|
|
@ -1,54 +0,0 @@
|
||||||
use std::env;
|
|
||||||
|
|
||||||
use argus_parser::{lexer, parser};
|
|
||||||
use ariadne::{sources, Color, Label, Report, ReportKind};
|
|
||||||
use chumsky::prelude::Input;
|
|
||||||
use chumsky::Parser;
|
|
||||||
|
|
||||||
fn main() {
|
|
||||||
let src = env::args().nth(1).expect("Expected expression");
|
|
||||||
|
|
||||||
let (tokens, errs) = lexer().parse(src.as_str()).into_output_errors();
|
|
||||||
|
|
||||||
println!("*** Outputting tokens ***");
|
|
||||||
if let Some(tokens) = &tokens {
|
|
||||||
for token in tokens {
|
|
||||||
println!("-> {:?}", token);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
let parse_errs = if let Some(tokens) = &tokens {
|
|
||||||
let (ast, parse_errs) = parser()
|
|
||||||
.map_with_span(|ast, span| (ast, span))
|
|
||||||
.parse(tokens.as_slice().spanned((src.len()..src.len()).into()))
|
|
||||||
.into_output_errors();
|
|
||||||
|
|
||||||
println!("*** Outputting tokens ***");
|
|
||||||
println!("{:#?}", ast);
|
|
||||||
|
|
||||||
parse_errs
|
|
||||||
} else {
|
|
||||||
Vec::new()
|
|
||||||
};
|
|
||||||
|
|
||||||
errs.into_iter()
|
|
||||||
.map(|e| e.map_token(|c| c.to_string()))
|
|
||||||
.chain(parse_errs.into_iter().map(|e| e.map_token(|tok| tok.to_string())))
|
|
||||||
.for_each(|e| {
|
|
||||||
Report::build(ReportKind::Error, src.clone(), e.span().start)
|
|
||||||
.with_message(e.to_string())
|
|
||||||
.with_label(
|
|
||||||
Label::new((src.clone(), e.span().into_range()))
|
|
||||||
.with_message(e.reason().to_string())
|
|
||||||
.with_color(Color::Red),
|
|
||||||
)
|
|
||||||
.with_labels(e.contexts().map(|(label, span)| {
|
|
||||||
Label::new((src.clone(), span.into_range()))
|
|
||||||
.with_message(format!("while parsing this {}", label))
|
|
||||||
.with_color(Color::Yellow)
|
|
||||||
}))
|
|
||||||
.finish()
|
|
||||||
.print(sources([(src.clone(), src.clone())]))
|
|
||||||
.unwrap()
|
|
||||||
});
|
|
||||||
}
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
||||||
[package]
|
|
||||||
name = "argus-semantics"
|
|
||||||
version = "0.1.1"
|
|
||||||
|
|
||||||
authors.workspace = true
|
|
||||||
license.workspace = true
|
|
||||||
edition.workspace = true
|
|
||||||
rust-version.workspace = true
|
|
||||||
readme.workspace = true
|
|
||||||
repository.workspace = true
|
|
||||||
|
|
||||||
[dependencies]
|
|
||||||
argus-core = { version = "0.1.1", path = "../argus-core" }
|
|
||||||
itertools = "0.11"
|
|
||||||
num-traits = "0.2.16"
|
|
||||||
paste = "1.0.14"
|
|
||||||
|
|
||||||
[dev-dependencies]
|
|
||||||
argus-core = { path = "../argus-core", features = ["arbitrary"] }
|
|
||||||
proptest = "1.2"
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
||||||
//! Argus offline semantics
|
|
||||||
//!
|
|
||||||
//! In this crate, we are predominantly concerned with the monitoring of _offline system
|
|
||||||
//! traces_, i.e., a collection of signals that have been extracted from observing and
|
|
||||||
//! sampling from some system.
|
|
||||||
|
|
||||||
pub mod semantics;
|
|
||||||
pub mod traits;
|
|
||||||
pub mod utils;
|
|
||||||
|
|
||||||
pub use semantics::{BooleanSemantics, QuantitativeSemantics};
|
|
||||||
pub use traits::Trace;
|
|
||||||
|
|
@ -1,5 +0,0 @@
|
||||||
mod boolean;
|
|
||||||
mod quantitative;
|
|
||||||
|
|
||||||
pub use boolean::BooleanSemantics;
|
|
||||||
pub use quantitative::QuantitativeSemantics;
|
|
||||||
|
|
@ -9,6 +9,26 @@ rust-version.workspace = true
|
||||||
readme.workspace = true
|
readme.workspace = true
|
||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
argus-core = { version = "0.1.1", path = "../argus-core" }
|
argus-derive = { version = "0.1.0", path = "../argus-derive" }
|
||||||
argus-parser = { version = "0.1.1", path = "../argus-parser" }
|
ariadne = { version = "0.3.0", optional = true }
|
||||||
argus-semantics = { version = "0.1.1", path = "../argus-semantics" }
|
chumsky = { version = "1.0.0-alpha.4", features = ["default", "label"] }
|
||||||
|
derive_more = "0.99.17"
|
||||||
|
enum_dispatch = "0.3.12"
|
||||||
|
itertools = "0.11"
|
||||||
|
num-traits = "0.2.16"
|
||||||
|
paste = "1.0.14"
|
||||||
|
proptest = { version = "1.2", optional = true }
|
||||||
|
thiserror = "1.0.47"
|
||||||
|
|
||||||
|
[dev-dependencies]
|
||||||
|
proptest = "1.2"
|
||||||
|
argus = { path = ".", features = ["arbitrary"] }
|
||||||
|
|
||||||
|
[features]
|
||||||
|
default = []
|
||||||
|
arbitrary = ["dep:proptest"]
|
||||||
|
reporting = ["dep:ariadne"]
|
||||||
|
|
||||||
|
[[example]]
|
||||||
|
name = "dump_expr"
|
||||||
|
required-features = ["reporting"]
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
use std::env;
|
use std::env;
|
||||||
|
|
||||||
use argus_parser::parse_str;
|
use argus::parse_str;
|
||||||
use ariadne::{sources, Color, Label, Report, ReportKind};
|
use ariadne::{sources, Color, Label, Report, ReportKind};
|
||||||
|
|
||||||
fn main() {
|
fn main() {
|
||||||
|
|
@ -15,6 +15,26 @@ pub use traits::*;
|
||||||
use self::iter::AstIter;
|
use self::iter::AstIter;
|
||||||
use crate::{ArgusResult, Error};
|
use crate::{ArgusResult, Error};
|
||||||
|
|
||||||
|
/// A trait representing expressions
|
||||||
|
#[enum_dispatch]
|
||||||
|
pub trait AnyExpr {
|
||||||
|
/// Check if the given expression is a numeric expression
|
||||||
|
fn is_numeric(&self) -> bool;
|
||||||
|
/// Check if the given expression is a boolean expression
|
||||||
|
fn is_boolean(&self) -> bool;
|
||||||
|
/// Get the arguments to the current expression.
|
||||||
|
///
|
||||||
|
/// If the expression doesn't contain arguments (i.e., it is a leaf expression) then
|
||||||
|
/// the vector is empty.
|
||||||
|
fn args(&self) -> Vec<ExprRef<'_>>;
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Marker trait for numeric expressions
|
||||||
|
pub trait IsNumExpr: AnyExpr + Into<NumExpr> {}
|
||||||
|
|
||||||
|
/// Marker trait for Boolean expressions
|
||||||
|
pub trait IsBoolExpr: AnyExpr + Into<BoolExpr> {}
|
||||||
|
|
||||||
/// All expressions that are numeric
|
/// All expressions that are numeric
|
||||||
#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
|
#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
|
||||||
#[enum_dispatch(AnyExpr)]
|
#[enum_dispatch(AnyExpr)]
|
||||||
1
argus/src/core/expr/traits.rs
Normal file
1
argus/src/core/expr/traits.rs
Normal file
|
|
@ -0,0 +1 @@
|
||||||
|
|
||||||
15
argus/src/core/mod.rs
Normal file
15
argus/src/core/mod.rs
Normal file
|
|
@ -0,0 +1,15 @@
|
||||||
|
//! # `argus-core`
|
||||||
|
//!
|
||||||
|
//! This crate provides some of the core functionality or interfaces for the other Argus
|
||||||
|
//! components. Mainly, the crate provides:
|
||||||
|
//!
|
||||||
|
//! 1. Expression tree nodes for defining temporal logic specifications (see [`expr`]).
|
||||||
|
//! 2. Different signal types for generating traces of data (see [`signals`]).
|
||||||
|
//! 3. A list of possible errors any component in Argus can generate (see
|
||||||
|
//! [`enum@Error`]).
|
||||||
|
|
||||||
|
pub mod expr;
|
||||||
|
pub mod signals;
|
||||||
|
|
||||||
|
pub use expr::*;
|
||||||
|
pub use signals::Signal;
|
||||||
103
argus/src/lib.rs
103
argus/src/lib.rs
|
|
@ -1,4 +1,99 @@
|
||||||
pub use argus_core::signals::{AnySignal, Signal};
|
#![warn(missing_docs)]
|
||||||
pub use argus_core::{expr, signals, ArgusResult, Error};
|
#![doc = include_str!("../../README.md")]
|
||||||
pub use argus_parser::parse_str;
|
|
||||||
pub use argus_semantics::{BooleanSemantics, QuantitativeSemantics, Trace};
|
extern crate self as argus;
|
||||||
|
|
||||||
|
mod core;
|
||||||
|
pub mod parser;
|
||||||
|
mod semantics;
|
||||||
|
|
||||||
|
use std::time::Duration;
|
||||||
|
|
||||||
|
use thiserror::Error;
|
||||||
|
|
||||||
|
pub use crate::core::signals::{AnySignal, Signal};
|
||||||
|
pub use crate::core::{expr, signals};
|
||||||
|
pub use crate::parser::parse_str;
|
||||||
|
pub use crate::semantics::{BooleanSemantics, QuantitativeSemantics, Trace};
|
||||||
|
|
||||||
|
/// Errors generated by all Argus components.
|
||||||
|
#[derive(Error, Debug)]
|
||||||
|
pub enum Error {
|
||||||
|
/// An identifier has been redeclared in a specification.
|
||||||
|
///
|
||||||
|
/// This is called mainly from [`expr::ExprBuilder`].
|
||||||
|
#[error("redeclaration of identifier")]
|
||||||
|
IdentifierRedeclaration,
|
||||||
|
|
||||||
|
/// An expression is provided with an insufficient number of arguments.
|
||||||
|
///
|
||||||
|
/// This is called for N-ary expressions:
|
||||||
|
/// [`NumExpr::Add`](crate::expr::NumExpr::Add),
|
||||||
|
/// [`NumExpr::Mul`](crate::expr::NumExpr::Mul),
|
||||||
|
/// [`BoolExpr::And`](crate::expr::BoolExpr::And), and
|
||||||
|
/// [`BoolExpr::Or`](crate::expr::BoolExpr::Or).
|
||||||
|
#[error("insufficient number of arguments")]
|
||||||
|
IncompleteArgs,
|
||||||
|
|
||||||
|
/// Attempting to `push` a new sample to a non-sampled signal
|
||||||
|
/// ([`Signal::Empty`](crate::signals::Signal::Empty) or
|
||||||
|
/// [`Signal::Constant`](crate::signals::Signal::Constant)).
|
||||||
|
#[error("cannot push value to non-sampled signal")]
|
||||||
|
InvalidPushToSignal,
|
||||||
|
|
||||||
|
/// Pushing the new value to the sampled signal makes it not strictly monotonically
|
||||||
|
/// increasing.
|
||||||
|
#[error(
|
||||||
|
"trying to create a non-monotonically signal, signal end time ({end_time:?}) > sample time point \
|
||||||
|
({current_sample:?})"
|
||||||
|
)]
|
||||||
|
NonMonotonicSignal {
|
||||||
|
/// The time that the signal actually ends
|
||||||
|
end_time: Duration,
|
||||||
|
/// The time point of the new (erroneous) sample.
|
||||||
|
current_sample: Duration,
|
||||||
|
},
|
||||||
|
|
||||||
|
/// Attempting to perform an invalid operation on a signal
|
||||||
|
#[error("invalid operation on signal")]
|
||||||
|
InvalidOperation,
|
||||||
|
|
||||||
|
/// Attempting to index a signal not present in a trace.
|
||||||
|
#[error("name not in signal trace")]
|
||||||
|
SignalNotPresent,
|
||||||
|
|
||||||
|
/// Attempting to perform a signal operation not supported by the type
|
||||||
|
#[error("incorrect signal type")]
|
||||||
|
InvalidSignalType,
|
||||||
|
|
||||||
|
/// Incorrect cast of signal
|
||||||
|
#[error("invalid cast from {from} to {to}")]
|
||||||
|
InvalidCast {
|
||||||
|
/// Type of the signal being cast from
|
||||||
|
from: &'static str,
|
||||||
|
/// Type of the signal being cast to
|
||||||
|
to: &'static str,
|
||||||
|
},
|
||||||
|
|
||||||
|
/// Invalid interval
|
||||||
|
#[error("invalid interval: {reason}")]
|
||||||
|
InvalidInterval {
|
||||||
|
/// Reason for interval being invalid
|
||||||
|
reason: &'static str,
|
||||||
|
},
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Error {
|
||||||
|
/// An [`InvalidCast`](Error::InvalidCast) error from `T` to `U`.
|
||||||
|
pub fn invalid_cast<T, U>() -> Self {
|
||||||
|
Self::InvalidCast {
|
||||||
|
from: std::any::type_name::<T>(),
|
||||||
|
to: std::any::type_name::<U>(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Alias for [`Error`](enum@Error)
|
||||||
|
pub type ArgusError = Error;
|
||||||
|
/// Alias for [`Result<T, ArgusError>`]
|
||||||
|
pub type ArgusResult<T> = Result<T, Error>;
|
||||||
|
|
|
||||||
|
|
@ -2,9 +2,9 @@ use std::fmt;
|
||||||
|
|
||||||
use chumsky::prelude::*;
|
use chumsky::prelude::*;
|
||||||
|
|
||||||
pub type Span = SimpleSpan<usize>;
|
pub(crate) type Span = SimpleSpan<usize>;
|
||||||
pub type Output<'a> = Vec<(Token<'a>, Span)>;
|
pub(crate) type Output<'a> = Vec<(Token<'a>, Span)>;
|
||||||
pub type Error<'a> = extra::Err<Rich<'a, char, Span>>;
|
pub(crate) type Error<'a> = extra::Err<Rich<'a, char, Span>>;
|
||||||
|
|
||||||
#[derive(Clone, Debug, PartialEq)]
|
#[derive(Clone, Debug, PartialEq)]
|
||||||
pub enum Token<'src> {
|
pub enum Token<'src> {
|
||||||
|
|
@ -1,16 +1,17 @@
|
||||||
//! # Argus logic syntax
|
//! # crate::core logic syntax
|
||||||
|
|
||||||
use std::time::Duration;
|
use std::time::Duration;
|
||||||
|
|
||||||
use argus_core::ExprBuilder;
|
use crate::core::expr::ExprBuilder;
|
||||||
mod lexer;
|
mod lexer;
|
||||||
mod parser;
|
mod syntax;
|
||||||
|
|
||||||
use chumsky::prelude::Rich;
|
use chumsky::prelude::Rich;
|
||||||
pub use lexer::{lexer, Error as LexError, Span, Token};
|
use lexer::{lexer, Token};
|
||||||
pub use parser::{parser, Expr, Interval};
|
use syntax::{parser, Expr, Interval};
|
||||||
|
|
||||||
pub fn parse_str(src: &str) -> Result<argus_core::Expr, Vec<Rich<'_, String>>> {
|
/// Parse a string expression into a concrete Argus expression.
|
||||||
|
pub fn parse_str(src: &str) -> Result<crate::core::expr::Expr, Vec<Rich<'_, String>>> {
|
||||||
use chumsky::prelude::{Input, Parser};
|
use chumsky::prelude::{Input, Parser};
|
||||||
|
|
||||||
let (tokens, lex_errors) = lexer().parse(src).into_output_errors();
|
let (tokens, lex_errors) = lexer().parse(src).into_output_errors();
|
||||||
|
|
@ -48,7 +49,7 @@ pub fn parse_str(src: &str) -> Result<argus_core::Expr, Vec<Rich<'_, String>>> {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn interval_convert(interval: &Interval<'_>) -> argus_core::Interval {
|
fn interval_convert(interval: &Interval<'_>) -> crate::core::expr::Interval {
|
||||||
use core::ops::Bound;
|
use core::ops::Bound;
|
||||||
let a = if let Some(a) = &interval.a {
|
let a = if let Some(a) = &interval.a {
|
||||||
match &a.0 {
|
match &a.0 {
|
||||||
|
|
@ -68,15 +69,15 @@ fn interval_convert(interval: &Interval<'_>) -> argus_core::Interval {
|
||||||
} else {
|
} else {
|
||||||
Bound::Unbounded
|
Bound::Unbounded
|
||||||
};
|
};
|
||||||
argus_core::Interval::new(a, b)
|
crate::core::expr::Interval::new(a, b)
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Convert a parsed [`Expr`] into an [Argus `Expr`](argus_core::Expr)
|
/// Convert a parsed [`Expr`] into an [crate::core `Expr`](crate::core::expr::Expr)
|
||||||
fn ast_to_expr<'tokens, 'src: 'tokens>(
|
fn ast_to_expr<'tokens, 'src: 'tokens>(
|
||||||
ast: &Expr<'src>,
|
ast: &Expr<'src>,
|
||||||
span: lexer::Span,
|
span: lexer::Span,
|
||||||
ctx: &mut ExprBuilder,
|
ctx: &mut ExprBuilder,
|
||||||
) -> Result<argus_core::Expr, Rich<'tokens, Token<'src>, lexer::Span>> {
|
) -> Result<crate::core::expr::Expr, Rich<'tokens, Token<'src>, lexer::Span>> {
|
||||||
match ast {
|
match ast {
|
||||||
Expr::Error => unreachable!("Errors should have been caught by parser"),
|
Expr::Error => unreachable!("Errors should have been caught by parser"),
|
||||||
Expr::Bool(value) => Ok(ctx.bool_const(*value).into()),
|
Expr::Bool(value) => Ok(ctx.bool_const(*value).into()),
|
||||||
|
|
@ -84,20 +85,20 @@ fn ast_to_expr<'tokens, 'src: 'tokens>(
|
||||||
Expr::UInt(value) => Ok(ctx.uint_const(*value).into()),
|
Expr::UInt(value) => Ok(ctx.uint_const(*value).into()),
|
||||||
Expr::Float(value) => Ok(ctx.float_const(*value).into()),
|
Expr::Float(value) => Ok(ctx.float_const(*value).into()),
|
||||||
Expr::Var { name, kind } => match kind {
|
Expr::Var { name, kind } => match kind {
|
||||||
parser::Type::Unknown => Err(Rich::custom(span, "All variables must have defined type by now.")),
|
syntax::Type::Unknown => Err(Rich::custom(span, "All variables must have defined type by now.")),
|
||||||
parser::Type::Bool => ctx
|
syntax::Type::Bool => ctx
|
||||||
.bool_var(name.to_string())
|
.bool_var(name.to_string())
|
||||||
.map(|var| var.into())
|
.map(|var| var.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string())),
|
.map_err(|err| Rich::custom(span, err.to_string())),
|
||||||
parser::Type::UInt => ctx
|
syntax::Type::UInt => ctx
|
||||||
.uint_var(name.to_string())
|
.uint_var(name.to_string())
|
||||||
.map(|var| var.into())
|
.map(|var| var.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string())),
|
.map_err(|err| Rich::custom(span, err.to_string())),
|
||||||
parser::Type::Int => ctx
|
syntax::Type::Int => ctx
|
||||||
.int_var(name.to_string())
|
.int_var(name.to_string())
|
||||||
.map(|var| var.into())
|
.map(|var| var.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string())),
|
.map_err(|err| Rich::custom(span, err.to_string())),
|
||||||
parser::Type::Float => ctx
|
syntax::Type::Float => ctx
|
||||||
.float_var(name.to_string())
|
.float_var(name.to_string())
|
||||||
.map(|var| var.into())
|
.map(|var| var.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string())),
|
.map_err(|err| Rich::custom(span, err.to_string())),
|
||||||
|
|
@ -106,23 +107,23 @@ fn ast_to_expr<'tokens, 'src: 'tokens>(
|
||||||
let arg = ast_to_expr(&arg.0, arg.1, ctx)?;
|
let arg = ast_to_expr(&arg.0, arg.1, ctx)?;
|
||||||
let interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span));
|
let interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span));
|
||||||
match op {
|
match op {
|
||||||
parser::UnaryOps::Neg => {
|
syntax::UnaryOps::Neg => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let argus_core::Expr::Num(arg) = arg else {
|
let crate::core::expr::Expr::Num(arg) = arg else {
|
||||||
unreachable!("- must have numeric expression argument");
|
unreachable!("- must have numeric expression argument");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_neg(Box::new(arg)).into())
|
Ok(ctx.make_neg(Box::new(arg)).into())
|
||||||
}
|
}
|
||||||
parser::UnaryOps::Not => {
|
syntax::UnaryOps::Not => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let argus_core::Expr::Bool(arg) = arg else {
|
let crate::core::expr::Expr::Bool(arg) = arg else {
|
||||||
unreachable!("`Not` must have boolean expression argument");
|
unreachable!("`Not` must have boolean expression argument");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_not(Box::new(arg)).into())
|
Ok(ctx.make_not(Box::new(arg)).into())
|
||||||
}
|
}
|
||||||
parser::UnaryOps::Next => {
|
syntax::UnaryOps::Next => {
|
||||||
use core::ops::Bound;
|
use core::ops::Bound;
|
||||||
let argus_core::Expr::Bool(arg) = arg else {
|
let crate::core::expr::Expr::Bool(arg) = arg else {
|
||||||
unreachable!("`Next` must have boolean expression argument");
|
unreachable!("`Next` must have boolean expression argument");
|
||||||
};
|
};
|
||||||
match interval {
|
match interval {
|
||||||
|
|
@ -141,8 +142,8 @@ fn ast_to_expr<'tokens, 'src: 'tokens>(
|
||||||
None => Ok(ctx.make_next(Box::new(arg)).into()),
|
None => Ok(ctx.make_next(Box::new(arg)).into()),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
parser::UnaryOps::Always => {
|
syntax::UnaryOps::Always => {
|
||||||
let argus_core::Expr::Bool(arg) = arg else {
|
let crate::core::expr::Expr::Bool(arg) = arg else {
|
||||||
unreachable!("`Always` must have boolean expression argument");
|
unreachable!("`Always` must have boolean expression argument");
|
||||||
};
|
};
|
||||||
match interval {
|
match interval {
|
||||||
|
|
@ -150,8 +151,8 @@ fn ast_to_expr<'tokens, 'src: 'tokens>(
|
||||||
None => Ok(ctx.make_always(Box::new(arg)).into()),
|
None => Ok(ctx.make_always(Box::new(arg)).into()),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
parser::UnaryOps::Eventually => {
|
syntax::UnaryOps::Eventually => {
|
||||||
let argus_core::Expr::Bool(arg) = arg else {
|
let crate::core::expr::Expr::Bool(arg) = arg else {
|
||||||
unreachable!("`Eventually` must have boolean expression argument");
|
unreachable!("`Eventually` must have boolean expression argument");
|
||||||
};
|
};
|
||||||
match interval {
|
match interval {
|
||||||
|
|
@ -171,127 +172,127 @@ fn ast_to_expr<'tokens, 'src: 'tokens>(
|
||||||
let interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span));
|
let interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span));
|
||||||
|
|
||||||
match op {
|
match op {
|
||||||
parser::BinaryOps::Add => {
|
syntax::BinaryOps::Add => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Add` must have numeric expression arguments");
|
unreachable!("`Add` must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_add([lhs, rhs])
|
ctx.make_add([lhs, rhs])
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Sub => {
|
syntax::BinaryOps::Sub => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Sub` must have numeric expression arguments");
|
unreachable!("`Sub` must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_sub(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_sub(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Mul => {
|
syntax::BinaryOps::Mul => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Mul` must have numeric expression arguments");
|
unreachable!("`Mul` must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_mul([lhs, rhs])
|
ctx.make_mul([lhs, rhs])
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Div => {
|
syntax::BinaryOps::Div => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Div` must have numeric expression arguments");
|
unreachable!("`Div` must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_div(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_div(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Lt => {
|
syntax::BinaryOps::Lt => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("Relational operation must have numeric expression arguments");
|
unreachable!("Relational operation must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_lt(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_lt(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Le => {
|
syntax::BinaryOps::Le => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("Relational operation must have numeric expression arguments");
|
unreachable!("Relational operation must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_le(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_le(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Gt => {
|
syntax::BinaryOps::Gt => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("Relational operation must have numeric expression arguments");
|
unreachable!("Relational operation must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_gt(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_gt(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Ge => {
|
syntax::BinaryOps::Ge => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("Relational operation must have numeric expression arguments");
|
unreachable!("Relational operation must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_ge(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_ge(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Eq => {
|
syntax::BinaryOps::Eq => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("Relational operation must have numeric expression arguments");
|
unreachable!("Relational operation must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_eq(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_eq(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Neq => {
|
syntax::BinaryOps::Neq => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Num(lhs), crate::core::expr::Expr::Num(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("Relational operation must have numeric expression arguments");
|
unreachable!("Relational operation must have numeric expression arguments");
|
||||||
};
|
};
|
||||||
Ok(ctx.make_neq(Box::new(lhs), Box::new(rhs)).into())
|
Ok(ctx.make_neq(Box::new(lhs), Box::new(rhs)).into())
|
||||||
}
|
}
|
||||||
parser::BinaryOps::And => {
|
syntax::BinaryOps::And => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`And` must have boolean expression arguments");
|
unreachable!("`And` must have boolean expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_and([lhs, rhs])
|
ctx.make_and([lhs, rhs])
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Or => {
|
syntax::BinaryOps::Or => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Or` must have boolean expression arguments");
|
unreachable!("`Or` must have boolean expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_or([lhs, rhs])
|
ctx.make_or([lhs, rhs])
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Implies => {
|
syntax::BinaryOps::Implies => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Implies` must have boolean expression arguments");
|
unreachable!("`Implies` must have boolean expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_implies(Box::new(lhs), Box::new(rhs))
|
ctx.make_implies(Box::new(lhs), Box::new(rhs))
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Equiv => {
|
syntax::BinaryOps::Equiv => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Equiv` must have boolean expression arguments");
|
unreachable!("`Equiv` must have boolean expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_equiv(Box::new(lhs), Box::new(rhs))
|
ctx.make_equiv(Box::new(lhs), Box::new(rhs))
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Xor => {
|
syntax::BinaryOps::Xor => {
|
||||||
assert!(interval.is_none());
|
assert!(interval.is_none());
|
||||||
let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Xor` must have boolean expression arguments");
|
unreachable!("`Xor` must have boolean expression arguments");
|
||||||
};
|
};
|
||||||
ctx.make_xor(Box::new(lhs), Box::new(rhs))
|
ctx.make_xor(Box::new(lhs), Box::new(rhs))
|
||||||
.map(|ex| ex.into())
|
.map(|ex| ex.into())
|
||||||
.map_err(|err| Rich::custom(span, err.to_string()))
|
.map_err(|err| Rich::custom(span, err.to_string()))
|
||||||
}
|
}
|
||||||
parser::BinaryOps::Until => {
|
syntax::BinaryOps::Until => {
|
||||||
let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
|
let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else {
|
||||||
unreachable!("`Until` must have boolean expression arguments");
|
unreachable!("`Until` must have boolean expression arguments");
|
||||||
};
|
};
|
||||||
match interval {
|
match interval {
|
||||||
|
|
@ -2,7 +2,7 @@ use chumsky::input::SpannedInput;
|
||||||
use chumsky::prelude::*;
|
use chumsky::prelude::*;
|
||||||
use chumsky::Parser;
|
use chumsky::Parser;
|
||||||
|
|
||||||
use crate::lexer::{Span, Token};
|
use super::lexer::{Span, Token};
|
||||||
|
|
||||||
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
|
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
|
||||||
pub enum Type {
|
pub enum Type {
|
||||||
|
|
@ -1,17 +1,18 @@
|
||||||
use std::ops::Bound;
|
use std::ops::Bound;
|
||||||
use std::time::Duration;
|
use std::time::Duration;
|
||||||
|
|
||||||
use argus_core::expr::*;
|
use super::utils::lemire_minmax::MonoWedge;
|
||||||
use argus_core::prelude::*;
|
use super::Trace;
|
||||||
use argus_core::signals::{InterpolationMethod, SignalPartialOrd};
|
use crate::core::expr::*;
|
||||||
|
use crate::core::signals::{InterpolationMethod, SignalPartialOrd};
|
||||||
use crate::semantics::QuantitativeSemantics;
|
use crate::semantics::QuantitativeSemantics;
|
||||||
use crate::traits::Trace;
|
use crate::{ArgusError, ArgusResult, Signal};
|
||||||
use crate::utils::lemire_minmax::MonoWedge;
|
|
||||||
|
|
||||||
|
/// Boolean semantics for Signal Temporal Logic expressionsd define by an [`Expr`].
|
||||||
pub struct BooleanSemantics;
|
pub struct BooleanSemantics;
|
||||||
|
|
||||||
impl BooleanSemantics {
|
impl BooleanSemantics {
|
||||||
|
/// Evaluates a [Boolean expression](BoolExpr) given a [`Trace`].
|
||||||
pub fn eval<BoolI, NumI>(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult<Signal<bool>>
|
pub fn eval<BoolI, NumI>(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult<Signal<bool>>
|
||||||
where
|
where
|
||||||
BoolI: InterpolationMethod<bool>,
|
BoolI: InterpolationMethod<bool>,
|
||||||
|
|
@ -24,7 +25,7 @@ impl BooleanSemantics {
|
||||||
.ok_or(ArgusError::SignalNotPresent)?
|
.ok_or(ArgusError::SignalNotPresent)?
|
||||||
.clone(),
|
.clone(),
|
||||||
BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
|
BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
|
||||||
use argus_core::expr::Ordering::*;
|
use crate::core::expr::Ordering::*;
|
||||||
let lhs = QuantitativeSemantics::eval_num_expr::<f64, NumI>(lhs, trace)?;
|
let lhs = QuantitativeSemantics::eval_num_expr::<f64, NumI>(lhs, trace)?;
|
||||||
let rhs = QuantitativeSemantics::eval_num_expr::<f64, NumI>(rhs, trace)?;
|
let rhs = QuantitativeSemantics::eval_num_expr::<f64, NumI>(rhs, trace)?;
|
||||||
|
|
||||||
|
|
@ -374,12 +375,12 @@ fn compute_untimed_until<I: InterpolationMethod<bool>>(
|
||||||
mod tests {
|
mod tests {
|
||||||
use std::collections::HashMap;
|
use std::collections::HashMap;
|
||||||
|
|
||||||
use argus_core::expr::ExprBuilder;
|
|
||||||
use argus_core::signals::interpolation::Linear;
|
|
||||||
use argus_core::signals::AnySignal;
|
|
||||||
use itertools::assert_equal;
|
use itertools::assert_equal;
|
||||||
|
|
||||||
use super::*;
|
use super::*;
|
||||||
|
use crate::core::expr::ExprBuilder;
|
||||||
|
use crate::core::signals::interpolation::Linear;
|
||||||
|
use crate::core::signals::AnySignal;
|
||||||
|
|
||||||
#[derive(Default)]
|
#[derive(Default)]
|
||||||
struct MyTrace {
|
struct MyTrace {
|
||||||
|
|
@ -1,6 +1,17 @@
|
||||||
//! Traits to define semantics for temporal logic specifications
|
//! Argus offline semantics
|
||||||
|
//!
|
||||||
|
//! In this crate, we are predominantly concerned with the monitoring of _offline system
|
||||||
|
//! traces_, i.e., a collection of signals that have been extracted from observing and
|
||||||
|
//! sampling from some system.
|
||||||
|
|
||||||
use argus_core::prelude::*;
|
mod boolean;
|
||||||
|
mod quantitative;
|
||||||
|
pub mod utils;
|
||||||
|
|
||||||
|
pub use boolean::BooleanSemantics;
|
||||||
|
pub use quantitative::QuantitativeSemantics;
|
||||||
|
|
||||||
|
use crate::Signal;
|
||||||
|
|
||||||
/// A trace is a collection of signals
|
/// A trace is a collection of signals
|
||||||
///
|
///
|
||||||
|
|
@ -9,8 +20,7 @@ use argus_core::prelude::*;
|
||||||
/// An example of a `Trace` may be:
|
/// An example of a `Trace` may be:
|
||||||
///
|
///
|
||||||
/// ```rust
|
/// ```rust
|
||||||
/// use argus_core::signals::{Signal, AnySignal};
|
/// use argus::{Signal, AnySignal, Trace};
|
||||||
/// use argus_semantics::Trace;
|
|
||||||
///
|
///
|
||||||
/// struct MyTrace {
|
/// struct MyTrace {
|
||||||
/// x: Signal<bool>,
|
/// x: Signal<bool>,
|
||||||
|
|
@ -1,17 +1,19 @@
|
||||||
use std::ops::Bound;
|
use std::ops::Bound;
|
||||||
use std::time::Duration;
|
use std::time::Duration;
|
||||||
|
|
||||||
use argus_core::expr::*;
|
|
||||||
use argus_core::prelude::*;
|
|
||||||
use argus_core::signals::{InterpolationMethod, SignalAbs};
|
|
||||||
use num_traits::{Num, NumCast};
|
use num_traits::{Num, NumCast};
|
||||||
|
|
||||||
use crate::traits::Trace;
|
use super::utils::lemire_minmax::MonoWedge;
|
||||||
use crate::utils::lemire_minmax::MonoWedge;
|
use super::Trace;
|
||||||
|
use crate::core::expr::*;
|
||||||
|
use crate::core::signals::{InterpolationMethod, SignalAbs};
|
||||||
|
use crate::{ArgusError, ArgusResult, Signal};
|
||||||
|
|
||||||
|
/// Quantitative semantics for Signal Temporal Logic expressionsd define by an [`Expr`].
|
||||||
pub struct QuantitativeSemantics;
|
pub struct QuantitativeSemantics;
|
||||||
|
|
||||||
impl QuantitativeSemantics {
|
impl QuantitativeSemantics {
|
||||||
|
/// Evaluates a [Boolean expression](BoolExpr) given a [`Trace`].
|
||||||
pub fn eval<I>(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult<Signal<f64>>
|
pub fn eval<I>(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult<Signal<f64>>
|
||||||
where
|
where
|
||||||
I: InterpolationMethod<f64>,
|
I: InterpolationMethod<f64>,
|
||||||
|
|
@ -23,7 +25,7 @@ impl QuantitativeSemantics {
|
||||||
.ok_or(ArgusError::SignalNotPresent)
|
.ok_or(ArgusError::SignalNotPresent)
|
||||||
.map(top_or_bot)?,
|
.map(top_or_bot)?,
|
||||||
BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
|
BoolExpr::Cmp(Cmp { op, lhs, rhs }) => {
|
||||||
use argus_core::expr::Ordering::*;
|
use crate::core::expr::Ordering::*;
|
||||||
let lhs = Self::eval_num_expr::<f64, I>(lhs, trace)?;
|
let lhs = Self::eval_num_expr::<f64, I>(lhs, trace)?;
|
||||||
let rhs = Self::eval_num_expr::<f64, I>(rhs, trace)?;
|
let rhs = Self::eval_num_expr::<f64, I>(rhs, trace)?;
|
||||||
|
|
||||||
|
|
@ -80,6 +82,7 @@ impl QuantitativeSemantics {
|
||||||
Ok(ret)
|
Ok(ret)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Evaluates a [numeric expression](NumExpr) given a [`Trace`].
|
||||||
pub fn eval_num_expr<T, I>(root: &NumExpr, trace: &impl Trace) -> ArgusResult<Signal<T>>
|
pub fn eval_num_expr<T, I>(root: &NumExpr, trace: &impl Trace) -> ArgusResult<Signal<T>>
|
||||||
where
|
where
|
||||||
T: Num + NumCast + Clone + PartialOrd,
|
T: Num + NumCast + Clone + PartialOrd,
|
||||||
|
|
@ -434,12 +437,12 @@ mod tests {
|
||||||
use std::iter::zip;
|
use std::iter::zip;
|
||||||
use std::time::Duration;
|
use std::time::Duration;
|
||||||
|
|
||||||
use argus_core::expr::ExprBuilder;
|
|
||||||
use argus_core::signals::interpolation::{Constant, Linear};
|
|
||||||
use argus_core::signals::AnySignal;
|
|
||||||
use itertools::assert_equal;
|
use itertools::assert_equal;
|
||||||
|
|
||||||
use super::*;
|
use super::*;
|
||||||
|
use crate::core::expr::ExprBuilder;
|
||||||
|
use crate::core::signals::interpolation::{Constant, Linear};
|
||||||
|
use crate::core::signals::AnySignal;
|
||||||
|
|
||||||
const FLOAT_EPS: f64 = 1.0e-8;
|
const FLOAT_EPS: f64 = 1.0e-8;
|
||||||
|
|
||||||
0
argus/src/semantics/traits.rs
Normal file
0
argus/src/semantics/traits.rs
Normal file
|
|
@ -69,6 +69,7 @@ impl<'a, T> MonoWedge<'a, T>
|
||||||
where
|
where
|
||||||
T: PartialOrd,
|
T: PartialOrd,
|
||||||
{
|
{
|
||||||
|
#[allow(dead_code)]
|
||||||
pub fn min_wedge(duration: Duration) -> Self {
|
pub fn min_wedge(duration: Duration) -> Self {
|
||||||
Self::new(duration, T::lt)
|
Self::new(duration, T::lt)
|
||||||
}
|
}
|
||||||
Loading…
Add table
Add a link
Reference in a new issue