From d89dbd4d943c7811d703d0f2217108e9a912f03e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Philipp=20Schro=CC=88er?= Date: Tue, 5 Nov 2024 22:44:15 +0100 Subject: [PATCH] jani: several additional impls --- jani/src/exprs.rs | 57 +++++++++++++++++++++++++++++++++--------- jani/src/properties.rs | 14 +++++------ jani/src/types.rs | 10 ++++---- 3 files changed, 57 insertions(+), 24 deletions(-) diff --git a/jani/src/exprs.rs b/jani/src/exprs.rs index afb69fd8..724026c1 100644 --- a/jani/src/exprs.rs +++ b/jani/src/exprs.rs @@ -10,7 +10,7 @@ pub use serde_json::Number; /// Mathematical constants that cannot be expressed using numeric values and /// basic jani-model expressions. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum MathConstant { /// Euler's number (the base of the natural logarithm); type real. #[serde(rename = "e")] @@ -29,7 +29,7 @@ impl Display for MathConstant { } } -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] #[serde(untagged)] pub enum ConstantValue { /// Numeric value; has type int if it is an integer and type real otherwise. @@ -41,9 +41,30 @@ pub enum ConstantValue { MathConstant(MathConstant), } -impl ConstantValue { - pub fn from_f64(value: f64) -> ConstantValue { - ConstantValue::Number(serde_json::Number::from_f64(value).unwrap()) +impl From for ConstantValue { + fn from(value: u64) -> Self { + ConstantValue::Number(value.into()) + } +} + +/// This error is emitted from the [`TryFrom`] implementation for +/// [`ConstantValue`] if the value is not finie (e.g. NaN or infinity). +#[derive(Debug)] +pub struct NotFiniteNumberError; + +impl TryFrom for ConstantValue { + type Error = NotFiniteNumberError; + + fn try_from(value: f64) -> Result { + serde_json::Number::from_f64(value) + .map(ConstantValue::Number) + .ok_or(NotFiniteNumberError) + } +} + +impl From for ConstantValue { + fn from(value: bool) -> Self { + ConstantValue::Boolean(value) } } @@ -63,7 +84,7 @@ impl Display for ConstantValue { /// `right`, or the type of `right` if that is assignable from the type of `left` /// (previously: the result type is the most specific type assignable from the /// types of then and else). -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] #[serde(tag = "op", rename = "ite")] pub struct IteExpression { #[serde(rename = "if")] @@ -75,7 +96,7 @@ pub struct IteExpression { } /// JANI operators with one operand. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum UnaryOp { /// Negation: computes `¬exp`. #[serde(rename = "¬")] @@ -94,14 +115,14 @@ pub enum UnaryOp { } /// JANI expressions with one operand. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] pub struct UnaryExpression { pub op: UnaryOp, pub exp: Expression, } /// JANI operators with two operands. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum BinaryOp { #[serde(rename = "∨")] Or, @@ -144,7 +165,7 @@ pub enum BinaryOp { } /// JANI expressions with two operands. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] pub struct BinaryExpression { pub op: BinaryOp, pub left: Expression, @@ -153,7 +174,7 @@ pub struct BinaryExpression { /// Nondeterministic selection (needs /// [`super::models::ModelFeature::NondetSelection`]). -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] #[serde(tag = "op", rename = "nondet")] pub struct NondetSelectionExpression { var: Identifier, @@ -161,7 +182,7 @@ pub struct NondetSelectionExpression { } /// JANI expressions. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] #[serde(untagged)] pub enum Expression { Constant(ConstantValue), @@ -173,4 +194,16 @@ pub enum Expression { NondetSelection(Box), } +impl From for Expression { + fn from(value: ConstantValue) -> Self { + Expression::Constant(value) + } +} + +impl From for Expression { + fn from(id: Identifier) -> Self { + Expression::Identifier(id) + } +} + pub type LValue = Identifier; diff --git a/jani/src/properties.rs b/jani/src/properties.rs index 74c57e00..792b97e2 100644 --- a/jani/src/properties.rs +++ b/jani/src/properties.rs @@ -19,7 +19,7 @@ pub struct PropertyInterval { pub type RewardAccumulation = Vec; -#[derive(Serialize, Deserialize, Debug, Clone, Copy)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] #[serde(rename_all = "kebab-case")] pub enum Reward { Steps, @@ -28,7 +28,7 @@ pub enum Reward { Exit, } -#[derive(Serialize, Deserialize, Debug, Clone, Copy)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] #[serde(rename_all = "lowercase")] pub enum FilterFun { Min, @@ -54,7 +54,7 @@ pub struct FilterExpression { pub states: Box, } -#[derive(Serialize, Deserialize, Debug, Clone, Copy)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum Quantifier { #[serde(rename = "Pmin")] Pmin, @@ -72,7 +72,7 @@ pub struct QuantifiedExpression { pub exp: Box, } -#[derive(Serialize, Deserialize, Debug, Clone, Copy)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum UntilExpressionKind { #[serde(rename = "U")] Until, @@ -104,7 +104,7 @@ pub struct UntilExpression { pub reward_bounds: Option>, } -#[derive(Serialize, Deserialize, Debug, Clone, Copy)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum UnaryPathExpressionKind { #[serde(rename = "F")] Finally, @@ -125,7 +125,7 @@ pub struct UnaryPathExpression { pub reward_bounds: Option>, } -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] pub enum ExpectedValueKind { Emin, Emax, @@ -156,7 +156,7 @@ pub struct ExpectedValueExpression { pub reward_instants: Option>, } -#[derive(Serialize, Deserialize, Debug, Clone, Copy)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] #[serde(tag = "op", rename_all = "kebab-case")] pub enum StatePredicate { Initial, diff --git a/jani/src/types.rs b/jani/src/types.rs index 35da9a1e..2cb0b1e0 100644 --- a/jani/src/types.rs +++ b/jani/src/types.rs @@ -4,7 +4,7 @@ use serde::{Deserialize, Serialize}; use crate::exprs::Expression; -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] #[serde(rename_all = "lowercase")] pub enum BasicType { /// Booleans, assignable from booleans only. @@ -17,7 +17,7 @@ pub enum BasicType { /// Numeric if `base` is numeric; `lower_bound` or `upper_bound` must be /// present. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] #[serde(tag = "kind", rename = "bounded", rename_all = "kebab-case")] pub struct BoundedType { pub base: BoundedTypeBase, @@ -37,7 +37,7 @@ impl BoundedType { } /// Subset of [`BasicType`]s for [`BoundedType`]s. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] #[serde(rename_all = "lowercase")] pub enum BoundedTypeBase { Int, @@ -45,7 +45,7 @@ pub enum BoundedTypeBase { } /// Other types for specific kinds of models. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, Copy, PartialEq, Eq)] #[serde(rename_all = "lowercase")] pub enum OtherType { /// Numeric; only allowed for TA, PTA, STA, HA, PHA and SHA; assignable from int and bounded int. @@ -60,7 +60,7 @@ pub enum OtherType { /// /// We represent types as an enum of other enums to simplify the serde /// implementations. -#[derive(Serialize, Deserialize, Debug, Clone)] +#[derive(Serialize, Deserialize, Debug, Clone, PartialEq, Eq)] #[serde(untagged)] pub enum Type { BasicType(BasicType),