diff --git a/Cargo.toml b/Cargo.toml index 3c61754..15c3453 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,13 +1,5 @@ [workspace] -members = [ - "argus", - "argus-core", - "argus-semantics", - "argus-derive", - "argus-parser", - "argus-automata", - "pyargus", -] +members = ["argus", "argus-derive", "argus-automata", "pyargus"] resolver = "2" diff --git a/argus-core/Cargo.toml b/argus-core/Cargo.toml deleted file mode 100644 index 2420a7d..0000000 --- a/argus-core/Cargo.toml +++ /dev/null @@ -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"] diff --git a/argus-core/src/expr/traits.rs b/argus-core/src/expr/traits.rs deleted file mode 100644 index 71cf057..0000000 --- a/argus-core/src/expr/traits.rs +++ /dev/null @@ -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>; -} - -/// Marker trait for numeric expressions -pub trait IsNumExpr: AnyExpr + Into {} - -/// Marker trait for Boolean expressions -pub trait IsBoolExpr: AnyExpr + Into {} diff --git a/argus-core/src/lib.rs b/argus-core/src/lib.rs deleted file mode 100644 index f419d91..0000000 --- a/argus-core/src/lib.rs +++ /dev/null @@ -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() -> Self { - Self::InvalidCast { - from: std::any::type_name::(), - to: std::any::type_name::(), - } - } -} - -/// Alias for [`Error`](enum@Error) -pub type ArgusError = Error; -/// Alias for [`Result`] -pub type ArgusResult = Result; diff --git a/argus-core/src/prelude.rs b/argus-core/src/prelude.rs deleted file mode 100644 index bc5739a..0000000 --- a/argus-core/src/prelude.rs +++ /dev/null @@ -1,5 +0,0 @@ -#![doc(hidden)] - -pub use crate::expr::*; -pub use crate::signals::Signal; -pub use crate::{ArgusError, ArgusResult}; diff --git a/argus-derive/src/expr/bool_expr.rs b/argus-derive/src/expr/bool_expr.rs index 478295a..56ddff9 100644 --- a/argus-derive/src/expr/bool_expr.rs +++ b/argus-derive/src/expr/bool_expr.rs @@ -3,12 +3,12 @@ use proc_macro2::{Ident, Span}; use quote::{quote, ToTokens}; 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. pub fn bool_expr_impl(input: DeriveInput) -> TokenStream { let ident = &input.ident; 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); @@ -29,11 +29,11 @@ fn impl_bool_not(input: &DeriveInput) -> impl ToTokens { let ident = &input.ident; quote! { impl ::core::ops::Not for #ident { - type Output = ::argus_core::expr::BoolExpr; + type Output = ::argus::expr::BoolExpr; #[inline] 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! { impl ::core::ops::#trait_name for #ident { - type Output = ::argus_core::expr::BoolExpr; + type Output = ::argus::expr::BoolExpr; #[inline] fn #trait_fn(self, other: Self) -> Self::Output { - use ::argus_core::expr::BoolExpr; - use ::argus_core::expr::#enum_id; + use ::argus::expr::BoolExpr; + use ::argus::expr::#enum_id; let lhs: BoolExpr = self.into(); let rhs: BoolExpr = other.into(); diff --git a/argus-derive/src/expr/num_expr.rs b/argus-derive/src/expr/num_expr.rs index b99b1a5..7524373 100644 --- a/argus-derive/src/expr/num_expr.rs +++ b/argus-derive/src/expr/num_expr.rs @@ -3,12 +3,12 @@ use proc_macro2::{Ident, Span}; use quote::{quote, ToTokens}; 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. pub fn num_expr_impl(input: DeriveInput) -> TokenStream { let ident = &input.ident; 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); @@ -33,11 +33,11 @@ fn impl_num_neg(input: &DeriveInput) -> impl ToTokens { let ident = &input.ident; quote! { impl ::core::ops::Neg for #ident { - type Output = ::argus_core::expr::NumExpr; + type Output = ::argus::expr::NumExpr; #[inline] 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! { impl ::core::ops::#trait_name for #ident 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] fn #trait_fn(self, other: T) -> Self::Output { - use ::argus_core::expr::NumExpr; - use ::argus_core::expr::#node_name; + use ::argus::expr::NumExpr; + use ::argus::expr::#node_name; let lhs: NumExpr = self.into(); let rhs: NumExpr = other.into(); @@ -115,13 +115,13 @@ fn impl_sub(input: &DeriveInput) -> impl ToTokens { quote! { impl ::core::ops::Sub for #ident 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] fn sub(self, other: T) -> Self::Output { - use ::argus_core::expr::Sub; + use ::argus::expr::Sub; let expr = Sub { lhs: Box::new(self.into()), rhs: Box::new(other.into()) @@ -137,13 +137,13 @@ fn impl_div(input: &DeriveInput) -> impl ToTokens { quote! { impl ::core::ops::Div for #ident 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] fn div(self, other: T) -> Self::Output { - use ::argus_core::expr::Div; + use ::argus::expr::Div; let expr = Div { dividend: Box::new(self.into()), divisor: Box::new(other.into()) diff --git a/argus-parser/Cargo.toml b/argus-parser/Cargo.toml deleted file mode 100644 index 1829a69..0000000 --- a/argus-parser/Cargo.toml +++ /dev/null @@ -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"] diff --git a/argus-parser/examples/dump_parse_tree.rs b/argus-parser/examples/dump_parse_tree.rs deleted file mode 100644 index 109b3fb..0000000 --- a/argus-parser/examples/dump_parse_tree.rs +++ /dev/null @@ -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() - }); -} diff --git a/argus-semantics/Cargo.toml b/argus-semantics/Cargo.toml deleted file mode 100644 index 450fd43..0000000 --- a/argus-semantics/Cargo.toml +++ /dev/null @@ -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" diff --git a/argus-semantics/src/lib.rs b/argus-semantics/src/lib.rs deleted file mode 100644 index 2e6319e..0000000 --- a/argus-semantics/src/lib.rs +++ /dev/null @@ -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; diff --git a/argus-semantics/src/semantics/mod.rs b/argus-semantics/src/semantics/mod.rs deleted file mode 100644 index 7f76a75..0000000 --- a/argus-semantics/src/semantics/mod.rs +++ /dev/null @@ -1,5 +0,0 @@ -mod boolean; -mod quantitative; - -pub use boolean::BooleanSemantics; -pub use quantitative::QuantitativeSemantics; diff --git a/argus/Cargo.toml b/argus/Cargo.toml index b38ac3f..6f63448 100644 --- a/argus/Cargo.toml +++ b/argus/Cargo.toml @@ -9,6 +9,26 @@ rust-version.workspace = true readme.workspace = true [dependencies] -argus-core = { version = "0.1.1", path = "../argus-core" } -argus-parser = { version = "0.1.1", path = "../argus-parser" } -argus-semantics = { version = "0.1.1", path = "../argus-semantics" } +argus-derive = { version = "0.1.0", path = "../argus-derive" } +ariadne = { version = "0.3.0", optional = true } +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"] diff --git a/argus-parser/examples/dump_expr.rs b/argus/examples/dump_expr.rs similarity index 97% rename from argus-parser/examples/dump_expr.rs rename to argus/examples/dump_expr.rs index 76e4c72..d608a8d 100644 --- a/argus-parser/examples/dump_expr.rs +++ b/argus/examples/dump_expr.rs @@ -1,6 +1,6 @@ use std::env; -use argus_parser::parse_str; +use argus::parse_str; use ariadne::{sources, Color, Label, Report, ReportKind}; fn main() { diff --git a/argus-core/proptest-regressions/expr/traits.txt b/argus/proptest-regressions/core/expr/traits.txt similarity index 100% rename from argus-core/proptest-regressions/expr/traits.txt rename to argus/proptest-regressions/core/expr/traits.txt diff --git a/argus-core/proptest-regressions/signals.txt b/argus/proptest-regressions/core/signals.txt similarity index 100% rename from argus-core/proptest-regressions/signals.txt rename to argus/proptest-regressions/core/signals.txt diff --git a/argus-semantics/proptest-regressions/utils/lemire_minmax.txt b/argus/proptest-regressions/semantics/utils/lemire_minmax.txt similarity index 100% rename from argus-semantics/proptest-regressions/utils/lemire_minmax.txt rename to argus/proptest-regressions/semantics/utils/lemire_minmax.txt diff --git a/argus-core/src/expr.rs b/argus/src/core/expr.rs similarity index 96% rename from argus-core/src/expr.rs rename to argus/src/core/expr.rs index 05baf79..d3f94e9 100644 --- a/argus-core/src/expr.rs +++ b/argus/src/core/expr.rs @@ -15,6 +15,26 @@ pub use traits::*; use self::iter::AstIter; 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>; +} + +/// Marker trait for numeric expressions +pub trait IsNumExpr: AnyExpr + Into {} + +/// Marker trait for Boolean expressions +pub trait IsBoolExpr: AnyExpr + Into {} + /// All expressions that are numeric #[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)] #[enum_dispatch(AnyExpr)] diff --git a/argus-core/src/expr/bool_expr.rs b/argus/src/core/expr/bool_expr.rs similarity index 100% rename from argus-core/src/expr/bool_expr.rs rename to argus/src/core/expr/bool_expr.rs diff --git a/argus-core/src/expr/iter.rs b/argus/src/core/expr/iter.rs similarity index 100% rename from argus-core/src/expr/iter.rs rename to argus/src/core/expr/iter.rs diff --git a/argus-core/src/expr/num_expr.rs b/argus/src/core/expr/num_expr.rs similarity index 100% rename from argus-core/src/expr/num_expr.rs rename to argus/src/core/expr/num_expr.rs diff --git a/argus/src/core/expr/traits.rs b/argus/src/core/expr/traits.rs new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/argus/src/core/expr/traits.rs @@ -0,0 +1 @@ + diff --git a/argus/src/core/mod.rs b/argus/src/core/mod.rs new file mode 100644 index 0000000..974eed0 --- /dev/null +++ b/argus/src/core/mod.rs @@ -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; diff --git a/argus-core/src/signals.rs b/argus/src/core/signals.rs similarity index 100% rename from argus-core/src/signals.rs rename to argus/src/core/signals.rs diff --git a/argus-core/src/signals/bool_ops.rs b/argus/src/core/signals/bool_ops.rs similarity index 100% rename from argus-core/src/signals/bool_ops.rs rename to argus/src/core/signals/bool_ops.rs diff --git a/argus-core/src/signals/cast.rs b/argus/src/core/signals/cast.rs similarity index 100% rename from argus-core/src/signals/cast.rs rename to argus/src/core/signals/cast.rs diff --git a/argus-core/src/signals/cmp_ops.rs b/argus/src/core/signals/cmp_ops.rs similarity index 100% rename from argus-core/src/signals/cmp_ops.rs rename to argus/src/core/signals/cmp_ops.rs diff --git a/argus-core/src/signals/interpolation.rs b/argus/src/core/signals/interpolation.rs similarity index 100% rename from argus-core/src/signals/interpolation.rs rename to argus/src/core/signals/interpolation.rs diff --git a/argus-core/src/signals/iter.rs b/argus/src/core/signals/iter.rs similarity index 100% rename from argus-core/src/signals/iter.rs rename to argus/src/core/signals/iter.rs diff --git a/argus-core/src/signals/num_ops.rs b/argus/src/core/signals/num_ops.rs similarity index 100% rename from argus-core/src/signals/num_ops.rs rename to argus/src/core/signals/num_ops.rs diff --git a/argus-core/src/signals/shift_ops.rs b/argus/src/core/signals/shift_ops.rs similarity index 100% rename from argus-core/src/signals/shift_ops.rs rename to argus/src/core/signals/shift_ops.rs diff --git a/argus-core/src/signals/traits.rs b/argus/src/core/signals/traits.rs similarity index 100% rename from argus-core/src/signals/traits.rs rename to argus/src/core/signals/traits.rs diff --git a/argus-core/src/signals/utils.rs b/argus/src/core/signals/utils.rs similarity index 100% rename from argus-core/src/signals/utils.rs rename to argus/src/core/signals/utils.rs diff --git a/argus/src/lib.rs b/argus/src/lib.rs index 3505898..8e6fa62 100644 --- a/argus/src/lib.rs +++ b/argus/src/lib.rs @@ -1,4 +1,99 @@ -pub use argus_core::signals::{AnySignal, Signal}; -pub use argus_core::{expr, signals, ArgusResult, Error}; -pub use argus_parser::parse_str; -pub use argus_semantics::{BooleanSemantics, QuantitativeSemantics, Trace}; +#![warn(missing_docs)] +#![doc = include_str!("../../README.md")] + +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() -> Self { + Self::InvalidCast { + from: std::any::type_name::(), + to: std::any::type_name::(), + } + } +} + +/// Alias for [`Error`](enum@Error) +pub type ArgusError = Error; +/// Alias for [`Result`] +pub type ArgusResult = Result; diff --git a/argus-parser/src/lexer.rs b/argus/src/parser/lexer.rs similarity index 97% rename from argus-parser/src/lexer.rs rename to argus/src/parser/lexer.rs index 5f35a43..917a3fb 100644 --- a/argus-parser/src/lexer.rs +++ b/argus/src/parser/lexer.rs @@ -2,9 +2,9 @@ use std::fmt; use chumsky::prelude::*; -pub type Span = SimpleSpan; -pub type Output<'a> = Vec<(Token<'a>, Span)>; -pub type Error<'a> = extra::Err>; +pub(crate) type Span = SimpleSpan; +pub(crate) type Output<'a> = Vec<(Token<'a>, Span)>; +pub(crate) type Error<'a> = extra::Err>; #[derive(Clone, Debug, PartialEq)] pub enum Token<'src> { diff --git a/argus-parser/src/lib.rs b/argus/src/parser/mod.rs similarity index 73% rename from argus-parser/src/lib.rs rename to argus/src/parser/mod.rs index 2121680..0b4a6c5 100644 --- a/argus-parser/src/lib.rs +++ b/argus/src/parser/mod.rs @@ -1,16 +1,17 @@ -//! # Argus logic syntax +//! # crate::core logic syntax use std::time::Duration; -use argus_core::ExprBuilder; +use crate::core::expr::ExprBuilder; mod lexer; -mod parser; +mod syntax; use chumsky::prelude::Rich; -pub use lexer::{lexer, Error as LexError, Span, Token}; -pub use parser::{parser, Expr, Interval}; +use lexer::{lexer, Token}; +use syntax::{parser, Expr, Interval}; -pub fn parse_str(src: &str) -> Result>> { +/// Parse a string expression into a concrete Argus expression. +pub fn parse_str(src: &str) -> Result>> { use chumsky::prelude::{Input, Parser}; let (tokens, lex_errors) = lexer().parse(src).into_output_errors(); @@ -48,7 +49,7 @@ pub fn parse_str(src: &str) -> Result>> { } } -fn interval_convert(interval: &Interval<'_>) -> argus_core::Interval { +fn interval_convert(interval: &Interval<'_>) -> crate::core::expr::Interval { use core::ops::Bound; let a = if let Some(a) = &interval.a { match &a.0 { @@ -68,15 +69,15 @@ fn interval_convert(interval: &Interval<'_>) -> argus_core::Interval { } else { 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>( ast: &Expr<'src>, span: lexer::Span, ctx: &mut ExprBuilder, -) -> Result, lexer::Span>> { +) -> Result, lexer::Span>> { match ast { Expr::Error => unreachable!("Errors should have been caught by parser"), 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::Float(value) => Ok(ctx.float_const(*value).into()), Expr::Var { name, kind } => match kind { - parser::Type::Unknown => Err(Rich::custom(span, "All variables must have defined type by now.")), - parser::Type::Bool => ctx + syntax::Type::Unknown => Err(Rich::custom(span, "All variables must have defined type by now.")), + syntax::Type::Bool => ctx .bool_var(name.to_string()) .map(|var| var.into()) .map_err(|err| Rich::custom(span, err.to_string())), - parser::Type::UInt => ctx + syntax::Type::UInt => ctx .uint_var(name.to_string()) .map(|var| var.into()) .map_err(|err| Rich::custom(span, err.to_string())), - parser::Type::Int => ctx + syntax::Type::Int => ctx .int_var(name.to_string()) .map(|var| var.into()) .map_err(|err| Rich::custom(span, err.to_string())), - parser::Type::Float => ctx + syntax::Type::Float => ctx .float_var(name.to_string()) .map(|var| var.into()) .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 interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span)); match op { - parser::UnaryOps::Neg => { + syntax::UnaryOps::Neg => { 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"); }; Ok(ctx.make_neg(Box::new(arg)).into()) } - parser::UnaryOps::Not => { + syntax::UnaryOps::Not => { 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"); }; Ok(ctx.make_not(Box::new(arg)).into()) } - parser::UnaryOps::Next => { + syntax::UnaryOps::Next => { 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"); }; match interval { @@ -141,8 +142,8 @@ fn ast_to_expr<'tokens, 'src: 'tokens>( None => Ok(ctx.make_next(Box::new(arg)).into()), } } - parser::UnaryOps::Always => { - let argus_core::Expr::Bool(arg) = arg else { + syntax::UnaryOps::Always => { + let crate::core::expr::Expr::Bool(arg) = arg else { unreachable!("`Always` must have boolean expression argument"); }; match interval { @@ -150,8 +151,8 @@ fn ast_to_expr<'tokens, 'src: 'tokens>( None => Ok(ctx.make_always(Box::new(arg)).into()), } } - parser::UnaryOps::Eventually => { - let argus_core::Expr::Bool(arg) = arg else { + syntax::UnaryOps::Eventually => { + let crate::core::expr::Expr::Bool(arg) = arg else { unreachable!("`Eventually` must have boolean expression argument"); }; 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)); match op { - parser::BinaryOps::Add => { + syntax::BinaryOps::Add => { 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"); }; ctx.make_add([lhs, rhs]) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Sub => { + syntax::BinaryOps::Sub => { 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"); }; Ok(ctx.make_sub(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Mul => { + syntax::BinaryOps::Mul => { 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"); }; ctx.make_mul([lhs, rhs]) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Div => { + syntax::BinaryOps::Div => { 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"); }; Ok(ctx.make_div(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Lt => { + syntax::BinaryOps::Lt => { 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"); }; Ok(ctx.make_lt(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Le => { + syntax::BinaryOps::Le => { 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"); }; Ok(ctx.make_le(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Gt => { + syntax::BinaryOps::Gt => { 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"); }; Ok(ctx.make_gt(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Ge => { + syntax::BinaryOps::Ge => { 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"); }; Ok(ctx.make_ge(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Eq => { + syntax::BinaryOps::Eq => { 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"); }; Ok(ctx.make_eq(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::Neq => { + syntax::BinaryOps::Neq => { 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"); }; Ok(ctx.make_neq(Box::new(lhs), Box::new(rhs)).into()) } - parser::BinaryOps::And => { + syntax::BinaryOps::And => { 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"); }; ctx.make_and([lhs, rhs]) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Or => { + syntax::BinaryOps::Or => { 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"); }; ctx.make_or([lhs, rhs]) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Implies => { + syntax::BinaryOps::Implies => { 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"); }; ctx.make_implies(Box::new(lhs), Box::new(rhs)) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Equiv => { + syntax::BinaryOps::Equiv => { 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"); }; ctx.make_equiv(Box::new(lhs), Box::new(rhs)) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Xor => { + syntax::BinaryOps::Xor => { 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"); }; ctx.make_xor(Box::new(lhs), Box::new(rhs)) .map(|ex| ex.into()) .map_err(|err| Rich::custom(span, err.to_string())) } - parser::BinaryOps::Until => { - let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else { + syntax::BinaryOps::Until => { + let (crate::core::expr::Expr::Bool(lhs), crate::core::expr::Expr::Bool(rhs)) = (lhs, rhs) else { unreachable!("`Until` must have boolean expression arguments"); }; match interval { diff --git a/argus-parser/src/parser.rs b/argus/src/parser/syntax.rs similarity index 99% rename from argus-parser/src/parser.rs rename to argus/src/parser/syntax.rs index cbce9a8..96ee83c 100644 --- a/argus-parser/src/parser.rs +++ b/argus/src/parser/syntax.rs @@ -2,7 +2,7 @@ use chumsky::input::SpannedInput; use chumsky::prelude::*; use chumsky::Parser; -use crate::lexer::{Span, Token}; +use super::lexer::{Span, Token}; #[derive(Debug, Clone, Copy, Default, PartialEq, Eq)] pub enum Type { diff --git a/argus-semantics/src/semantics/boolean.rs b/argus/src/semantics/boolean.rs similarity index 96% rename from argus-semantics/src/semantics/boolean.rs rename to argus/src/semantics/boolean.rs index e8298d7..435e68c 100644 --- a/argus-semantics/src/semantics/boolean.rs +++ b/argus/src/semantics/boolean.rs @@ -1,17 +1,18 @@ use std::ops::Bound; use std::time::Duration; -use argus_core::expr::*; -use argus_core::prelude::*; -use argus_core::signals::{InterpolationMethod, SignalPartialOrd}; - +use super::utils::lemire_minmax::MonoWedge; +use super::Trace; +use crate::core::expr::*; +use crate::core::signals::{InterpolationMethod, SignalPartialOrd}; use crate::semantics::QuantitativeSemantics; -use crate::traits::Trace; -use crate::utils::lemire_minmax::MonoWedge; +use crate::{ArgusError, ArgusResult, Signal}; +/// Boolean semantics for Signal Temporal Logic expressionsd define by an [`Expr`]. pub struct BooleanSemantics; impl BooleanSemantics { + /// Evaluates a [Boolean expression](BoolExpr) given a [`Trace`]. pub fn eval(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult> where BoolI: InterpolationMethod, @@ -24,7 +25,7 @@ impl BooleanSemantics { .ok_or(ArgusError::SignalNotPresent)? .clone(), BoolExpr::Cmp(Cmp { op, lhs, rhs }) => { - use argus_core::expr::Ordering::*; + use crate::core::expr::Ordering::*; let lhs = QuantitativeSemantics::eval_num_expr::(lhs, trace)?; let rhs = QuantitativeSemantics::eval_num_expr::(rhs, trace)?; @@ -374,12 +375,12 @@ fn compute_untimed_until>( mod tests { 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 super::*; + use crate::core::expr::ExprBuilder; + use crate::core::signals::interpolation::Linear; + use crate::core::signals::AnySignal; #[derive(Default)] struct MyTrace { diff --git a/argus-semantics/src/traits.rs b/argus/src/semantics/mod.rs similarity index 74% rename from argus-semantics/src/traits.rs rename to argus/src/semantics/mod.rs index e5f96d3..3ad4e72 100644 --- a/argus-semantics/src/traits.rs +++ b/argus/src/semantics/mod.rs @@ -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 /// @@ -9,8 +20,7 @@ use argus_core::prelude::*; /// An example of a `Trace` may be: /// /// ```rust -/// use argus_core::signals::{Signal, AnySignal}; -/// use argus_semantics::Trace; +/// use argus::{Signal, AnySignal, Trace}; /// /// struct MyTrace { /// x: Signal, diff --git a/argus-semantics/src/semantics/quantitative.rs b/argus/src/semantics/quantitative.rs similarity index 97% rename from argus-semantics/src/semantics/quantitative.rs rename to argus/src/semantics/quantitative.rs index 8ddaa54..2ab91d5 100644 --- a/argus-semantics/src/semantics/quantitative.rs +++ b/argus/src/semantics/quantitative.rs @@ -1,17 +1,19 @@ use std::ops::Bound; use std::time::Duration; -use argus_core::expr::*; -use argus_core::prelude::*; -use argus_core::signals::{InterpolationMethod, SignalAbs}; use num_traits::{Num, NumCast}; -use crate::traits::Trace; -use crate::utils::lemire_minmax::MonoWedge; +use super::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; impl QuantitativeSemantics { + /// Evaluates a [Boolean expression](BoolExpr) given a [`Trace`]. pub fn eval(expr: &BoolExpr, trace: &impl Trace) -> ArgusResult> where I: InterpolationMethod, @@ -23,7 +25,7 @@ impl QuantitativeSemantics { .ok_or(ArgusError::SignalNotPresent) .map(top_or_bot)?, BoolExpr::Cmp(Cmp { op, lhs, rhs }) => { - use argus_core::expr::Ordering::*; + use crate::core::expr::Ordering::*; let lhs = Self::eval_num_expr::(lhs, trace)?; let rhs = Self::eval_num_expr::(rhs, trace)?; @@ -80,6 +82,7 @@ impl QuantitativeSemantics { Ok(ret) } + /// Evaluates a [numeric expression](NumExpr) given a [`Trace`]. pub fn eval_num_expr(root: &NumExpr, trace: &impl Trace) -> ArgusResult> where T: Num + NumCast + Clone + PartialOrd, @@ -434,12 +437,12 @@ mod tests { use std::iter::zip; 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 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; diff --git a/argus/src/semantics/traits.rs b/argus/src/semantics/traits.rs new file mode 100644 index 0000000..e69de29 diff --git a/argus-semantics/src/utils.rs b/argus/src/semantics/utils.rs similarity index 100% rename from argus-semantics/src/utils.rs rename to argus/src/semantics/utils.rs diff --git a/argus-semantics/src/utils/lemire_minmax.rs b/argus/src/semantics/utils/lemire_minmax.rs similarity index 99% rename from argus-semantics/src/utils/lemire_minmax.rs rename to argus/src/semantics/utils/lemire_minmax.rs index 6439656..d662c23 100644 --- a/argus-semantics/src/utils/lemire_minmax.rs +++ b/argus/src/semantics/utils/lemire_minmax.rs @@ -69,6 +69,7 @@ impl<'a, T> MonoWedge<'a, T> where T: PartialOrd, { + #[allow(dead_code)] pub fn min_wedge(duration: Duration) -> Self { Self::new(duration, T::lt) }