From 4925fbf2e0fbe8c4a1329c6c2dd9092d1c029c9d Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Mon, 12 Feb 2024 12:14:35 +0100 Subject: [PATCH] upd data_reader --- Cargo.toml | 1 + src/data_reader/json_reader.rs | 10 +--- src/data_reader/parse_queries.rs | 10 ++-- src/data_reader/proto_reader.rs | 2 +- src/data_reader/serialization.rs | 93 +++++++++++++------------------- src/system/query_failures.rs | 15 +++--- 6 files changed, 52 insertions(+), 79 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index e946d9ca..7e11b767 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -46,6 +46,7 @@ itertools = "0.10.5" regex = "1" rayon = "1.6.1" lazy_static = "1.4.0" +num = "0.4.1" # Enable optimizations for EDBM in debug mode, but not for our code: [profile.dev.package.edbm] diff --git a/src/data_reader/json_reader.rs b/src/data_reader/json_reader.rs index acc05da7..ab77e1ec 100644 --- a/src/data_reader/json_reader.rs +++ b/src/data_reader/json_reader.rs @@ -31,15 +31,7 @@ pub fn read_json_component>( .join("Components") .join(format!("{}.json", component_name)); - let component: Result = match read_json(&component_path) { - Ok(json) => Ok(json), - Err(error) => Err(SyntaxFailure::unparsable( - error.to_string(), - component_path.display().to_string(), - )), - }; - - component + read_json(&component_path).map_err(|e| SyntaxFailure::unparseable(e, component_path.display())) } /// Opens a file and reads it. diff --git a/src/data_reader/parse_queries.rs b/src/data_reader/parse_queries.rs index 842f1b1a..961a20c1 100644 --- a/src/data_reader/parse_queries.rs +++ b/src/data_reader/parse_queries.rs @@ -34,10 +34,8 @@ pub fn parse_system(pair: pest::iterators::Pair) -> SystemExpression { SystemExpression::Component(comp_name, special_id) } - Rule::variable_name => { - let comp_name = pair.as_str().to_string(); - SystemExpression::Component(comp_name, None) - } + Rule::variable_name => SystemExpression::Component(pair.as_str().to_string(), None), + _ => unreachable!("Unexpected rule: {:?}", pair.as_rule()), }) .map_infix(|left, op, right| { @@ -201,9 +199,7 @@ fn parse_query(pair: pest::iterators::Pair) -> QueryExpression { QueryExpression::BisimMinim(SaveExpression { system, name }) } Rule::syntax => { - let mut pairs = pair.into_inner(); - let system = parse_system(pairs.next().unwrap()); - QueryExpression::Syntax(system) + QueryExpression::Syntax(parse_system(pair.into_inner().next().unwrap())) } _ => unreachable!("Unexpected rule: {:?}", pair.as_rule()), }; diff --git a/src/data_reader/proto_reader.rs b/src/data_reader/proto_reader.rs index 2b3dc92c..1542bda1 100644 --- a/src/data_reader/proto_reader.rs +++ b/src/data_reader/proto_reader.rs @@ -85,7 +85,7 @@ fn proto_location_tree_to_location_tree( ) -> Rc { let target: SpecificLocation = location_tree.into(); - system.construct_location_tree(target).unwrap() + system.construct_location_tree(target).unwrap() // TODO maybe handle `Err` better } fn proto_constraint_to_constraint( diff --git a/src/data_reader/serialization.rs b/src/data_reader/serialization.rs index 780dff29..c4b17bce 100644 --- a/src/data_reader/serialization.rs +++ b/src/data_reader/serialization.rs @@ -1,8 +1,9 @@ -use crate::data_reader::parse_edge; -use crate::model_objects::expressions; +use crate::data_reader::parse_edge::{parse_guard, parse_updates, Update}; +use crate::model_objects::expressions::{ArithExpression, BoolExpression}; use crate::model_objects::{Component, Declarations, Edge, Location, LocationType, SyncType}; use crate::simulation::graph_layout::layout_dummy_component; use edbm::util::constraints::ClockIndex; +use itertools::Itertools; use serde::{Deserialize, Deserializer, Serialize, Serializer}; use std::collections::HashMap; use std::ops::Add; @@ -45,12 +46,12 @@ pub struct DummyEdge { deserialize_with = "decode_guard", serialize_with = "encode_opt_boolexpr" )] - pub guard: Option, + pub guard: Option, #[serde( deserialize_with = "decode_update", serialize_with = "encode_opt_updates" )] - pub update: Option>, + pub update: Option>, #[serde(deserialize_with = "decode_sync")] pub sync: String, pub select: String, @@ -138,7 +139,7 @@ pub struct DummyLocation { //deserialize_with = "decode_invariant", serialize_with = "encode_opt_boolexpr" )] - pub invariant: Option, + pub invariant: Option, #[serde( //deserialize_with = "decode_location_type", serialize_with = "encode_location_type", @@ -180,12 +181,26 @@ pub fn decode_declarations<'de, D>(deserializer: D) -> Result, { + fn take_var_names( + dest: &mut HashMap, + counter: &mut T, + str: Vec, + ) { + for split_str in str.iter().skip(1) { + let comma_split: Vec = split_str.split(',').map(|s| s.into()).collect(); + for var in comma_split.into_iter().filter(|s| !s.is_empty()) { + dest.insert(var, *counter); + *counter = *counter + num::one(); + } + } + } let s = String::deserialize(deserializer)?; //Split string into vector of strings let decls: Vec = s.split('\n').map(|s| s.into()).collect(); let mut ints: HashMap = HashMap::new(); let mut clocks: HashMap = HashMap::new(); - let mut counter: ClockIndex = 1; + let mut clock_counter = 1; + let mut int_counter = 1; for string in decls { //skip comments if string.starts_with("//") || string.is_empty() { @@ -199,24 +214,9 @@ where let variable_type = split_string[0].as_str(); if variable_type == "clock" { - for split_str in split_string.iter().skip(1) { - let comma_split: Vec = - split_str.split(',').map(|s| s.into()).collect(); - for var in comma_split { - if !var.is_empty() { - clocks.insert(var, counter); - counter += 1; - } - } - } + take_var_names(&mut clocks, &mut clock_counter, split_string); } else if variable_type == "int" { - for split_str in split_string.iter().skip(1) { - let comma_split: Vec = - split_str.split(',').map(|s| s.into()).collect(); - for var in comma_split { - ints.insert(var, 0); - } - } + take_var_names(&mut ints, &mut int_counter, split_string); } else { panic!("Not implemented read for type: \"{}\"", variable_type); } @@ -228,9 +228,7 @@ where } /// Function used for deserializing guards -pub fn decode_guard<'de, D>( - deserializer: D, -) -> Result, D::Error> +pub fn decode_guard<'de, D>(deserializer: D) -> Result, D::Error> where D: Deserializer<'de>, { @@ -238,13 +236,13 @@ where if s.is_empty() { return Ok(None); } - parse_edge::parse_guard(&s).map(Some).map_err(|err| { + parse_guard(&s).map(Some).map_err(|err| { serde::de::Error::custom(format!("Could not parse {} got error: {:?}", s, err)) }) } //Function used for deserializing updates -pub fn decode_update<'de, D>(deserializer: D) -> Result>, D::Error> +pub fn decode_update<'de, D>(deserializer: D) -> Result>, D::Error> where D: Deserializer<'de>, { @@ -253,15 +251,13 @@ where return Ok(None); } - parse_edge::parse_updates(&s).map(Some).map_err(|err| { + parse_updates(&s).map(Some).map_err(|err| { serde::de::Error::custom(format!("Could not parse {} got error: {:?}", s, err)) }) } //Function used for deserializing invariants -pub fn decode_invariant<'de, D>( - deserializer: D, -) -> Result, D::Error> +pub fn decode_invariant<'de, D>(deserializer: D) -> Result, D::Error> where D: Deserializer<'de>, { @@ -269,7 +265,7 @@ where if s.is_empty() { return Ok(None); } - match parse_edge::parse_guard(&s) { + match parse_guard(&s) { Ok(edge_attribute) => Ok(Some(edge_attribute)), Err(e) => panic!("Could not parse invariant {} got error: {:?}", s, e), } @@ -350,23 +346,16 @@ pub fn encode_declarations(decls: &Declarations, serializer: S) -> Result( - opt_expr: &Option, + opt_expr: &Option, serializer: S, ) -> Result where @@ -379,20 +368,14 @@ where } } -pub fn encode_boolexpr( - expr: &expressions::BoolExpression, - serializer: S, -) -> Result +pub fn encode_boolexpr(expr: &BoolExpression, serializer: S) -> Result where S: Serializer, { serializer.serialize_str(&expr.encode_expr()) } -pub fn encode_arithexpr( - expr: &expressions::ArithExpression, - serializer: S, -) -> Result +pub fn encode_arithexpr(expr: &ArithExpression, serializer: S) -> Result where S: Serializer, { @@ -400,7 +383,7 @@ where } pub fn encode_opt_updates( - opt_updates: &Option>, + opt_updates: &Option>, serializer: S, ) -> Result where diff --git a/src/system/query_failures.rs b/src/system/query_failures.rs index 285c6437..10bc28ad 100644 --- a/src/system/query_failures.rs +++ b/src/system/query_failures.rs @@ -1,3 +1,4 @@ +use std::fmt::Display; use std::{collections::HashSet, fmt}; use crate::model_objects::{Component, State, StatePair}; @@ -527,10 +528,10 @@ pub enum SyntaxFailure { } impl SyntaxFailure { - pub fn unparsable(msg: impl Into, path: impl Into) -> SyntaxResult { + pub fn unparseable(msg: M, path: P) -> SyntaxResult { Err(SyntaxFailure::Unparsable { - msg: msg.into(), - path: path.into(), + msg: msg.to_string(), + path: path.to_string(), }) } } @@ -539,8 +540,8 @@ impl SyntaxFailure { // --- Format Display Impl --- // // ---------------------------- // -impl fmt::Display for DeterminismFailure { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> std::fmt::Result { +impl Display for DeterminismFailure { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!( f, "The system '{}' is not deterministic in state {} for {}", @@ -549,8 +550,8 @@ impl fmt::Display for DeterminismFailure { } } -impl fmt::Display for RefinementFailure { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { +impl Display for RefinementFailure { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { RefinementFailure::CutsDelaySolutions { system,