jani: several additional impls

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<u64> for ConstantValue {
+    fn from(value: u64) -> Self {
+        ConstantValue::Number(value.into())
+    }
+}
+
+/// This error is emitted from the [`TryFrom<f64>`] implementation for
+/// [`ConstantValue`] if the value is not finie (e.g. NaN or infinity).
+#[derive(Debug)]
+pub struct NotFiniteNumberError;
+
+impl TryFrom<f64> for ConstantValue {
+    type Error = NotFiniteNumberError;
+
+    fn try_from(value: f64) -> Result<Self, Self::Error> {
+        serde_json::Number::from_f64(value)
+            .map(ConstantValue::Number)
+            .ok_or(NotFiniteNumberError)
+    }
+}
+
+impl From<bool> 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,15 +174,15 @@ 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,
     exp: Expression,
 }
 
 /// 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<NondetSelectionExpression>),
 }
 
+impl From<ConstantValue> for Expression {
+    fn from(value: ConstantValue) -> Self {
+        Expression::Constant(value)
+    }
+}
+
+impl From<Identifier> for Expression {
+    fn from(id: Identifier) -> Self {
+        Expression::Identifier(id)
+    }
+}
+
 pub type LValue = Identifier;

jani/src/properties.rs

@@ -19,7 +19,7 @@ pub struct PropertyInterval {
 
 pub type RewardAccumulation = Vec<Reward>;
 
-#[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<PropertyExpression>,
 }
 
-#[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<PropertyExpression>,
 }
 
-#[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<Vec<RewardBound>>,
 }
 
-#[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<Vec<RewardBound>>,
 }
 
-#[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<Vec<RewardInstant>>,
 }
 
-#[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,

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,15 +37,15 @@ 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,
     Real,
 }
 
 /// 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),