diff --git a/.gitmodules b/.gitmodules index 0f1d640e..fa9c441f 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +1,4 @@ [submodule "Ecdar-ProtoBuf"] path = Ecdar-ProtoBuf url = https://github.com/Ecdar/Ecdar-ProtoBuf.git - branch = futureproof2 + branch = futureproof1 diff --git a/Ecdar-ProtoBuf b/Ecdar-ProtoBuf index ae8364e6..9b9ce8fd 160000 --- a/Ecdar-ProtoBuf +++ b/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit ae8364e6c8942a5cfde24adec779ca87d4431e4a +Subproject commit 9b9ce8fd52c14916d110667147e6421255b0c54d diff --git a/src/DataReader/component_loader.rs b/src/DataReader/component_loader.rs index 544d185b..d949e08c 100644 --- a/src/DataReader/component_loader.rs +++ b/src/DataReader/component_loader.rs @@ -1,10 +1,10 @@ use log::warn; use lru::LruCache; -use crate::component::Component; +use crate::component::Automaton; use crate::xml_parser; use crate::DataReader::json_reader; -use crate::DataReader::json_writer::component_to_json_file; +use crate::DataReader::json_writer::automaton_to_json_file; use crate::DataReader::xml_parser::parse_xml_from_file; use crate::ModelObjects::queries::Query; use crate::ModelObjects::system_declarations::SystemDeclarations; @@ -15,26 +15,26 @@ use std::collections::HashMap; use std::num::NonZeroUsize; use std::sync::{Arc, Mutex}; -use super::proto_reader::components_info_to_components; +use super::proto_reader::components_info_to_automata; -type ComponentsMap = HashMap; +type AutomataMap = HashMap; -struct ComponentTuple { - components_hash: u32, - components_map: Arc, +struct AutomataTuple { + automata_hash: u32, + automata_map: Arc, } /// A struct used for caching the models. #[derive(Debug, Clone)] pub struct ModelCache { // TODO: A concurrent lru may be faster to use and cause less prone to lock contention. - cache: Arc>>, + cache: Arc>>, } impl Default for ModelCache { fn default() -> Self { Self { - cache: Arc::new(Mutex::new(LruCache::::new( + cache: Arc::new(Mutex::new(LruCache::::new( NonZeroUsize::new(100).unwrap(), ))), } @@ -49,7 +49,7 @@ impl ModelCache { /// * `cache_size` - A number representing the number of users that can be cached simultaneusly. pub fn new(cache_size: usize) -> Self { Self { - cache: Arc::new(Mutex::new(LruCache::::new( + cache: Arc::new(Mutex::new(LruCache::::new( NonZeroUsize::new(cache_size).unwrap(), ))), } @@ -59,21 +59,21 @@ impl ModelCache { /// /// # Arguments /// - /// * `components_hash` - A hash of the components - pub fn get_model(&self, user_id: i32, components_hash: u32) -> Option { - if components_hash == 0 { - warn!("The component has no hash (0), so we assume it should not be cached."); + /// * `automata_hash` - A hash of the automata + pub fn get_model(&self, user_id: i32, automata_hash: u32) -> Option { + if automata_hash == 0 { + warn!("The automaton has no hash (0), so we assume it should not be cached."); return None; } let mut cache = self.cache.lock().unwrap(); - let components = cache.get(&user_id); + let automata = cache.get(&user_id); - components.and_then(|component_pair| { - if component_pair.components_hash == components_hash { - Some(ComponentContainer::new(Arc::clone( - &component_pair.components_map, + automata.and_then(|automata_pair| { + if automata_pair.automata_hash == automata_hash { + Some(AutomataContainer::new(Arc::clone( + &automata_pair.automata_map, ))) } else { None @@ -85,53 +85,53 @@ impl ModelCache { /// /// # Arguments /// - /// * `components_hash` - A hash of the components - /// * `container_components` - The `ComponentContainer's` loaded components (aka Model) to be cached. + /// * `automata_hash` - A hash of the automata + /// * `container_automata` - The `AutomataContainer's` loaded automata (aka Model) to be cached. pub fn insert_model( &mut self, user_id: i32, - components_hash: u32, - container_components: Arc, - ) -> ComponentContainer { - if components_hash == 0 { - warn!("The component has no hash (0), so we assume it should not be cached."); - return ComponentContainer::new(container_components); + automata_hash: u32, + container_automata: Arc, + ) -> AutomataContainer { + if automata_hash == 0 { + warn!("The automaton has no hash (0), so we assume it should not be cached."); + return AutomataContainer::new(container_automata); } self.cache.lock().unwrap().put( user_id, - ComponentTuple { - components_hash, - components_map: Arc::clone(&container_components), + AutomataTuple { + automata_hash, + automata_map: Arc::clone(&container_automata), }, ); - ComponentContainer::new(container_components) + AutomataContainer::new(container_automata) } } -pub trait ComponentLoader { - fn get_component(&mut self, component_name: &str) -> &Component; - fn save_component(&mut self, component: Component); +pub trait AutomataLoader { + fn get_automaton(&mut self, automaton_name: &str) -> &Automaton; + fn save_automaton(&mut self, automaton: Automaton); fn get_settings(&self) -> &Settings; } #[derive(Debug, Default, Clone)] -pub struct ComponentContainer { - pub loaded_components: Arc, +pub struct AutomataContainer { + pub loaded_automata: Arc, settings: Option, } -impl ComponentLoader for ComponentContainer { - fn get_component(&mut self, component_name: &str) -> &Component { - if let Some(component) = self.loaded_components.get(component_name) { - assert_eq!(component_name, component.get_name()); - component +impl AutomataLoader for AutomataContainer { + fn get_automaton(&mut self, automaton_name: &str) -> &Automaton { + if let Some(automaton) = self.loaded_automata.get(automaton_name) { + assert_eq!(automaton_name, automaton.get_name()); + automaton } else { - panic!("The component '{}' could not be retrieved", component_name); + panic!("The automaton '{}' could not be retrieved", automaton_name); } } - fn save_component(&mut self, _component: Component) { + fn save_automaton(&mut self, _automaton: Automaton) { //Intentionally left blank (no-op func) } @@ -140,33 +140,33 @@ impl ComponentLoader for ComponentContainer { } } -impl ComponentContainer { - pub fn new(map: Arc) -> Self { - ComponentContainer { - loaded_components: map, +impl AutomataContainer { + pub fn new(map: Arc) -> Self { + AutomataContainer { + loaded_automata: map, settings: None, } } - /// Creates a [`ComponentContainer`] from a [`services::ComponentsInfo`]. + /// Creates a [`AutomataContainer`] from a [`services::ComponentsInfo`]. pub fn from_info( components_info: &services::ComponentsInfo, - ) -> Result { - let components = components_info_to_components(components_info); - let component_container = Self::from_components(components); - Ok(component_container) + ) -> Result { + let automata = components_info_to_automata(components_info); + let automata_container = Self::from_automata(automata); + Ok(automata_container) } - /// Creates a [`ComponentContainer`] from a [`Vec`] of [`Component`]s - pub fn from_components(components: Vec) -> ComponentContainer { - let mut comp_hashmap = HashMap::::new(); - for mut component in components { - log::trace!("Adding comp {} to container", component.get_name()); - let inputs: Vec<_> = component.get_input_actions(); - input_enabler::make_input_enabled(&mut component, &inputs); - comp_hashmap.insert(component.get_name().to_string(), component); + /// Creates a [`AutomataContainer`] from a [`Vec`] of [`Automaton`]s + pub fn from_automata(automata: Vec) -> AutomataContainer { + let mut comp_hashmap = HashMap::::new(); + for mut automaton in automata { + log::trace!("Adding comp {} to container", automaton.get_name()); + let inputs: Vec<_> = automaton.get_input_actions(); + input_enabler::make_input_enabled(&mut automaton, &inputs); + comp_hashmap.insert(automaton.get_name().to_string(), automaton); } - ComponentContainer::new(Arc::new(comp_hashmap)) + AutomataContainer::new(Arc::new(comp_hashmap)) } /// Sets the settings @@ -175,66 +175,66 @@ impl ComponentContainer { } } -pub fn parse_components_if_some( +pub fn parse_automata_if_some( proto_component: &services::Component, -) -> Result, tonic::Status> { +) -> Result, tonic::Status> { if let Some(rep) = &proto_component.rep { match rep { - services::component::Rep::Json(json) => parse_json_component(json), - services::component::Rep::Xml(xml) => Ok(parse_xml_components(xml)), + services::component::Rep::Json(json) => parse_json_automaton(json), + services::component::Rep::Xml(xml) => Ok(parse_xml_automata(xml)), } } else { Ok(vec![]) } } -fn parse_json_component(json: &str) -> Result, tonic::Status> { - match json_reader::json_to_component(json) { +fn parse_json_automaton(json: &str) -> Result, tonic::Status> { + match json_reader::json_to_automaton(json) { Ok(comp) => Ok(vec![comp]), Err(_) => Err(tonic::Status::invalid_argument( - "Failed to parse json component", + "Failed to parse json automaton", )), } } -fn parse_xml_components(xml: &str) -> Vec { +fn parse_xml_automata(xml: &str) -> Vec { let (comps, _, _) = xml_parser::parse_xml_from_str(xml); comps } -pub trait ProjectLoader: ComponentLoader { +pub trait ProjectLoader: AutomataLoader { fn get_declarations(&self) -> &SystemDeclarations; fn get_queries(&self) -> &Vec; fn get_project_path(&self) -> &str; - fn to_comp_loader(self: Box) -> Box; + fn to_comp_loader(self: Box) -> Box; } pub struct JsonProjectLoader { project_path: String, - loaded_components: ComponentsMap, + loaded_automata: AutomataMap, system_declarations: SystemDeclarations, queries: Vec, settings: Settings, } -impl ComponentLoader for JsonProjectLoader { - fn get_component(&mut self, component_name: &str) -> &Component { - if !self.is_component_loaded(component_name) { - self.load_component(component_name); +impl AutomataLoader for JsonProjectLoader { + fn get_automaton(&mut self, automaton_name: &str) -> &Automaton { + if !self.is_automaton_loaded(automaton_name) { + self.load_automaton(automaton_name); } - if let Some(component) = self.loaded_components.get(component_name) { - assert_eq!(component_name, component.get_name()); - component + if let Some(automaton) = self.loaded_automata.get(automaton_name) { + assert_eq!(automaton_name, automaton.get_name()); + automaton } else { - panic!("The component '{}' could not be retrieved", component_name); + panic!("The automaton '{}' could not be retrieved", automaton_name); } } - fn save_component(&mut self, component: Component) { - component_to_json_file(&self.project_path, &component); - self.loaded_components - .insert(component.get_name().clone(), component); + fn save_automaton(&mut self, automaton: Automaton) { + automaton_to_json_file(&self.project_path, &automaton); + self.loaded_automata + .insert(automaton.get_name().clone(), automaton); } fn get_settings(&self) -> &Settings { @@ -255,7 +255,7 @@ impl ProjectLoader for JsonProjectLoader { &self.project_path } - fn to_comp_loader(self: Box) -> Box { + fn to_comp_loader(self: Box) -> Box { self } } @@ -267,52 +267,52 @@ impl JsonProjectLoader { Box::new(JsonProjectLoader { project_path, - loaded_components: HashMap::new(), + loaded_automata: HashMap::new(), system_declarations, queries, settings, }) } - fn load_component(&mut self, component_name: &str) { - let mut component = json_reader::read_json_component(&self.project_path, component_name); + fn load_automaton(&mut self, automaton_name: &str) { + let mut automaton = json_reader::read_json_automaton(&self.project_path, automaton_name); let opt_inputs = self .get_declarations() - .get_component_inputs(component.get_name()); + .get_automaton_inputs(automaton.get_name()); if let Some(inputs) = opt_inputs { - input_enabler::make_input_enabled(&mut component, inputs); + input_enabler::make_input_enabled(&mut automaton, inputs); } - self.loaded_components - .insert(String::from(component_name), component); + self.loaded_automata + .insert(String::from(automaton_name), automaton); } - fn is_component_loaded(&self, component_name: &str) -> bool { - self.loaded_components.contains_key(component_name) + fn is_automaton_loaded(&self, automaton_name: &str) -> bool { + self.loaded_automata.contains_key(automaton_name) } } pub struct XmlProjectLoader { project_path: String, - loaded_components: ComponentsMap, + loaded_automata: AutomataMap, system_declarations: SystemDeclarations, queries: Vec, settings: Settings, } -impl ComponentLoader for XmlProjectLoader { - fn get_component(&mut self, component_name: &str) -> &Component { - if let Some(component) = self.loaded_components.get(component_name) { - assert_eq!(component_name, component.get_name()); - component +impl AutomataLoader for XmlProjectLoader { + fn get_automaton(&mut self, automaton_name: &str) -> &Automaton { + if let Some(automaton) = self.loaded_automata.get(automaton_name) { + assert_eq!(automaton_name, automaton.get_name()); + automaton } else { - panic!("The component '{}' could not be retrieved", component_name); + panic!("The automaton '{}' could not be retrieved", automaton_name); } } - fn save_component(&mut self, _: Component) { - panic!("Saving components is not supported for XML projects") + fn save_automaton(&mut self, _: Automaton) { + panic!("Saving automata is not supported for XML projects") } fn get_settings(&self) -> &Settings { @@ -333,29 +333,29 @@ impl ProjectLoader for XmlProjectLoader { &self.project_path } - fn to_comp_loader(self: Box) -> Box { + fn to_comp_loader(self: Box) -> Box { self } } impl XmlProjectLoader { pub fn new_loader(project_path: String, settings: Settings) -> Box { - let (comps, system_declarations, queries) = parse_xml_from_file(&project_path); + let (automata, system_declarations, queries) = parse_xml_from_file(&project_path); - let mut map = HashMap::::new(); - for mut component in comps { - let opt_inputs = system_declarations.get_component_inputs(component.get_name()); + let mut map = HashMap::::new(); + for mut automaton in automata { + let opt_inputs = system_declarations.get_automaton_inputs(automaton.get_name()); if let Some(opt_inputs) = opt_inputs { - input_enabler::make_input_enabled(&mut component, opt_inputs); + input_enabler::make_input_enabled(&mut automaton, opt_inputs); } - let name = String::from(component.get_name()); - map.insert(name, component); + let name = String::from(automaton.get_name()); + map.insert(name, automaton); } Box::new(XmlProjectLoader { project_path, - loaded_components: map, + loaded_automata: map, system_declarations, queries, settings, diff --git a/src/DataReader/json_reader.rs b/src/DataReader/json_reader.rs index e8fe087f..29c91197 100644 --- a/src/DataReader/json_reader.rs +++ b/src/DataReader/json_reader.rs @@ -1,4 +1,4 @@ -use crate::ModelObjects::component; +use crate::component::Automaton; use crate::ModelObjects::queries; use crate::ModelObjects::system_declarations::SystemDeclarations; use serde::de::DeserializeOwned; @@ -20,29 +20,29 @@ pub fn read_system_declarations(project_path: &str) -> Option(&sysdecl_path) { Ok(sys_decls) => Some(sys_decls), Err(error) => panic!( - "We got error {}, and could not parse json file {} to component", + "We got error {}, and could not parse json file {} to automaton", error, &sysdecl_path ), } } -pub fn read_json_component(project_path: &str, component_name: &str) -> component::Component { - let component_path = format!( +pub fn read_json_automaton(project_path: &str, automaton_name: &str) -> Automaton { + let automaton_path = format!( "{0}{1}Components{1}{2}.json", project_path, std::path::MAIN_SEPARATOR, - component_name + automaton_name ); - let component: component::Component = match read_json(&component_path) { + let automaton: Automaton = match read_json(&automaton_path) { Ok(json) => json, Err(error) => panic!( - "We got error {}, and could not parse json file {} to component", - error, component_path + "We got error {}, and could not parse json file {} to automaton", + error, automaton_path ), }; - component + automaton } //Input:File name @@ -60,7 +60,7 @@ pub fn read_json(filename: &str) -> serde_json::Result { Ok(json_file) } -pub fn json_to_component(json_str: &str) -> Result { +pub fn json_to_automaton(json_str: &str) -> Result { serde_json::from_str(json_str) } diff --git a/src/DataReader/json_writer.rs b/src/DataReader/json_writer.rs index b5c4c83e..38e0cd95 100644 --- a/src/DataReader/json_writer.rs +++ b/src/DataReader/json_writer.rs @@ -1,18 +1,18 @@ -use crate::ModelObjects::component::Component; +use crate::ModelObjects::component::Automaton; use std::fs::File; -pub fn component_to_json_file(project_path: &str, component: &Component) { +pub fn automaton_to_json_file(project_path: &str, automaton: &Automaton) { let path = format!( "{0}{1}Components{1}{2}.json", project_path, std::path::MAIN_SEPARATOR, - component.get_name() + automaton.get_name() ); let file = File::create(path).expect("Couldnt open file"); - serde_json::to_writer_pretty(&file, component).expect("Failed to serialize component"); + serde_json::to_writer_pretty(&file, automaton).expect("Failed to serialize automaton"); } -pub fn component_to_json(component: &Component) -> String { - serde_json::to_string(component).unwrap() +pub fn automaton_to_json(automaton: &Automaton) -> String { + serde_json::to_string(automaton).unwrap() } diff --git a/src/DataReader/proto_reader.rs b/src/DataReader/proto_reader.rs index 2f8956f6..e54336a5 100644 --- a/src/DataReader/proto_reader.rs +++ b/src/DataReader/proto_reader.rs @@ -4,7 +4,8 @@ use std::convert::TryInto; use edbm::util::constraints::{Conjunction, Constraint, Disjunction, Inequality, RawInequality}; use edbm::zones::OwnedFederation; -use crate::component::{Component, Declarations, State}; +use crate::component::{Automaton, Declarations}; +use crate::ModelObjects::state::State; use crate::ProtobufServer::services::{ clock::Clock as ClockEnum, Clock as ProtoClock, ComponentsInfo, Constraint as ProtoConstraint, Decision as ProtoDecision, Disjunction as ProtoDisjunction, LocationTree as ProtoLocationTree, @@ -14,14 +15,14 @@ use crate::Simulation::decision::Decision; use crate::System::specifics::SpecificLocation; use crate::TransitionSystems::{LocationTree, TransitionSystemPtr}; -use super::component_loader::parse_components_if_some; +use super::component_loader::parse_automata_if_some; -/// Borrows a [`ComponentsInfo`] and returns the corresponding [`Vec`] of [`Component`]s. -pub fn components_info_to_components(components_info: &ComponentsInfo) -> Vec { +/// Borrows a [`ComponentsInfo`] and returns the corresponding [`Vec`] of [`Automaton`]. +pub fn components_info_to_automata(components_info: &ComponentsInfo) -> Vec { components_info .components .iter() - .flat_map(parse_components_if_some) + .flat_map(parse_automata_if_some) .flatten() .collect() } @@ -126,7 +127,7 @@ fn proto_zone_to_owned_federation( // Get the vector of conjunctions from the proto let proto_conjunctions = proto_zone.conjunctions; - // Generate map from component index to declarations (include component name for sanity check) + // Generate map from automaton index to declarations (include automaton name for sanity check) let infos = system.comp_infos(); let map = infos .iter() diff --git a/src/DataReader/serialization.rs b/src/DataReader/serialization.rs index ccd75126..170072d4 100644 --- a/src/DataReader/serialization.rs +++ b/src/DataReader/serialization.rs @@ -1,10 +1,11 @@ use crate::DataReader::parse_edge; use crate::DataReader::parse_invariant; -use crate::ModelObjects::component::{ - Component, Declarations, Edge, Location, LocationType, SyncType, -}; +use crate::ModelObjects::component::{Automaton, Declarations}; +use crate::ModelObjects::edge::Edge; +use crate::ModelObjects::edge::SyncType; +use crate::ModelObjects::location::{Location, LocationType}; use crate::ModelObjects::representations; -use crate::Simulation::graph_layout::layout_dummy_component; +use crate::Simulation::graph_layout::layout_dummy_automaton; use edbm::util::constraints::ClockIndex; use serde::{Deserialize, Deserializer, Serialize, Serializer}; use std::collections::HashMap; @@ -92,7 +93,7 @@ impl From for DummyEdge { } #[derive(Serialize)] -pub struct DummyComponent { +pub struct DummyAutomaton { pub name: String, #[serde( @@ -112,9 +113,9 @@ pub struct DummyComponent { pub height: f32, } -impl From for DummyComponent { - fn from(item: Component) -> Self { - let mut comp = DummyComponent { +impl From for DummyAutomaton { + fn from(item: Automaton) -> Self { + let mut comp = DummyAutomaton { name: item.name, declarations: item.declarations, locations: item.locations.into_iter().map(|l| l.into()).collect(), @@ -128,7 +129,7 @@ impl From for DummyComponent { height: 0.0, }; - layout_dummy_component(&mut comp); + layout_dummy_automaton(&mut comp); comp } diff --git a/src/DataReader/xml_parser.rs b/src/DataReader/xml_parser.rs index 54fbbbb4..8c927f82 100644 --- a/src/DataReader/xml_parser.rs +++ b/src/DataReader/xml_parser.rs @@ -1,8 +1,12 @@ +use crate::component::Automaton; use crate::DataReader::parse_edge::Update; use crate::DataReader::{parse_edge, parse_invariant}; -use crate::ModelObjects::component::{Declarations, Edge, LocationType, SyncType}; +use crate::ModelObjects::edge::Edge; +use crate::ModelObjects::location::{Location, LocationType}; +use crate::ModelObjects::queries; +use crate::ModelObjects::representations; use crate::ModelObjects::system_declarations::{SystemDeclarations, SystemSpecification}; -use crate::ModelObjects::{component, queries, representations, system_declarations}; +use crate::ModelObjects::{component::Declarations, edge::SyncType}; use edbm::util::constraints::ClockIndex; use elementtree::{Element, FindChildren}; use std::collections::HashMap; @@ -17,11 +21,7 @@ pub fn is_xml_project(project_path: &str) -> bool { ///Used to parse systems described in xml pub(crate) fn parse_xml_from_file( fileName: &str, -) -> ( - Vec, - system_declarations::SystemDeclarations, - Vec, -) { +) -> (Vec, SystemDeclarations, Vec) { //Open file and read xml let file = File::open(fileName).unwrap(); let reader = BufReader::new(file); @@ -31,40 +31,30 @@ pub(crate) fn parse_xml_from_file( pub(crate) fn parse_xml_from_str( xml: &str, -) -> ( - Vec, - system_declarations::SystemDeclarations, - Vec, -) { +) -> (Vec, SystemDeclarations, Vec) { let reader = BufReader::new(xml.as_bytes()); parse_xml(reader) } -fn parse_xml( - xml_data: R, -) -> ( - Vec, - system_declarations::SystemDeclarations, - Vec, -) { +fn parse_xml(xml_data: R) -> (Vec, SystemDeclarations, Vec) { let root = Element::from_reader(xml_data).unwrap(); - //storage of components - let mut xml_components: Vec = vec![]; + //storage of automata + let mut xml_automata: Vec = vec![]; - for xml_comp in root.find_all("template") { - let declarations = match xml_comp.find("declaration") { + for xml_automaton in root.find_all("template") { + let declarations = match xml_automaton.find("declaration") { Some(e) => parse_declarations(e.text()), None => parse_declarations(""), }; - let edges = collect_edges(xml_comp.find_all("transition")); - let comp = component::Component { - name: xml_comp.find("name").unwrap().text().parse().unwrap(), + let edges = collect_edges(xml_automaton.find_all("transition")); + let comp = Automaton { + name: xml_automaton.find("name").unwrap().text().parse().unwrap(), declarations, locations: collect_locations( - xml_comp.find_all("location"), - xml_comp + xml_automaton.find_all("location"), + xml_automaton .find("init") .expect("No initial location") .get_attr("ref") @@ -72,7 +62,7 @@ fn parse_xml( ), edges, }; - xml_components.push(comp); + xml_automata.push(comp); } let system_declarations = SystemDeclarations { @@ -80,13 +70,13 @@ fn parse_xml( declarations: decode_sync_type(root.find("system").unwrap().text()), }; - (xml_components, system_declarations, vec![]) + (xml_automata, system_declarations, vec![]) } -fn collect_locations(xml_locations: FindChildren, initial_id: &str) -> Vec { - let mut locations: Vec = vec![]; +fn collect_locations(xml_locations: FindChildren, initial_id: &str) -> Vec { + let mut locations: Vec = vec![]; for loc in xml_locations { - let location = component::Location { + let location = Location { id: loc.get_attr("id").unwrap().parse().unwrap(), invariant: match loc.find("label") { Some(x) => match parse_invariant::parse(x.text()) { @@ -108,7 +98,7 @@ fn collect_locations(xml_locations: FindChildren, initial_id: &str) -> Vec Vec { - let mut edges: Vec = vec![]; + let mut edges: Vec = vec![]; for e in xml_edges { let mut guard: Option = None; let mut updates: Option> = None; @@ -137,7 +127,7 @@ fn collect_edges(xml_edges: FindChildren) -> Vec { _ => {} } } - let edge = component::Edge { + let edge = Edge { id: "NotImplemented".to_string(), // We do not support edge IDs for XML right now. source_location: e .find("source") @@ -219,9 +209,9 @@ fn decode_sync_type(global_decl: &str) -> SystemSpecification { let decls: Vec = global_decl.split('\n').map(|s| s.into()).collect(); let mut input_actions: HashMap> = HashMap::new(); let mut output_actions: HashMap> = HashMap::new(); - let mut components: Vec = vec![]; + let mut automata: Vec = vec![]; - let mut component_names: Vec = vec![]; + let mut automata_names: Vec = vec![]; for declaration in &decls { //skip comments @@ -231,32 +221,32 @@ fn decode_sync_type(global_decl: &str) -> SystemSpecification { if !declaration.trim().is_empty() { if first_run { - let component_decls = declaration; + let automata_decls = declaration; - component_names = component_decls + automata_names = automata_decls .split(' ') .map(|s| s.chars().filter(|c| !c.is_whitespace()).collect()) .collect(); - if component_names[0] == "system" { + if automata_names[0] == "system" { //do not include element 0 as that is the system keyword - for name in component_names.iter_mut().skip(1) { + for name in automata_names.iter_mut().skip(1) { let s = name.replace(',', ""); let s_cleaned = s.replace(';', ""); *name = s_cleaned.clone(); - components.push(s_cleaned); + automata.push(s_cleaned); } first_run = false; } else { - panic!("Unexpected format of system declarations. Missing system in beginning of {:?}", component_names) + panic!("Unexpected format of system declarations. Missing system in beginning of {:?}", automata_names) } } let split_string: Vec = declaration.split(' ').map(|s| s.into()).collect(); if split_string[0].as_str() == "IO" { - let component_name = split_string[1].clone(); + let automaton_name = split_string[1].clone(); - if component_names.contains(&component_name) { + if automata_names.contains(&automaton_name) { for split_str in split_string.iter().skip(2) { let mut s = split_str.replace('{', ""); s = s.replace('\r', ""); @@ -269,19 +259,19 @@ fn decode_sync_type(global_decl: &str) -> SystemSpecification { } if action.ends_with('?') { let r = action.replace('?', ""); - if let Some(Channel_vec) = input_actions.get_mut(&component_name) { + if let Some(Channel_vec) = input_actions.get_mut(&automaton_name) { Channel_vec.push(r) } else { let Channel_vec = vec![r]; - input_actions.insert(component_name.clone(), Channel_vec); + input_actions.insert(automaton_name.clone(), Channel_vec); } } else if action.ends_with('!') { let r = action.replace('!', ""); - if let Some(Channel_vec) = output_actions.get_mut(&component_name) { + if let Some(Channel_vec) = output_actions.get_mut(&automaton_name) { Channel_vec.push(r.clone()) } else { let Channel_vec = vec![r.clone()]; - output_actions.insert(component_name.clone(), Channel_vec); + output_actions.insert(automaton_name.clone(), Channel_vec); } } else { panic!("Channel type not defined for Channel {:?}", action) @@ -289,13 +279,13 @@ fn decode_sync_type(global_decl: &str) -> SystemSpecification { } } } else { - panic!("Was not able to find component name: {:?} in declared component names: {:?}", component_name, component_names) + panic!("Was not able to find automaton name: {:?} in declared automata names: {:?}", automaton_name, automata_names) } } } } SystemSpecification { - components, + automata, input_actions, output_actions, } diff --git a/src/ModelObjects/component.rs b/src/ModelObjects/component.rs index 799fe038..e4676bfe 100644 --- a/src/ModelObjects/component.rs +++ b/src/ModelObjects/component.rs @@ -1,27 +1,20 @@ -use crate::DataReader::parse_edge; +use crate::DataReader::serialization::decode_declarations; +use crate::DataReader::serialization::DummyAutomaton; -use crate::DataReader::serialization::{ - decode_declarations, decode_guard, decode_invariant, decode_location_type, decode_sync, - decode_sync_type, decode_update, DummyComponent, DummyEdge, DummyLocation, -}; - -use crate::EdgeEval::constraint_applyer::apply_constraints_to_state; -use crate::EdgeEval::updater::CompiledUpdate; use edbm::util::bounds::Bounds; use edbm::util::constraints::ClockIndex; -use crate::ModelObjects::representations::BoolExpression; -use crate::TransitionSystems::{CompositionType, TransitionSystem}; -use crate::TransitionSystems::{LocationTree, TransitionID}; -use edbm::zones::OwnedFederation; +use crate::ModelObjects::edge::{Edge, SyncType}; +use crate::ModelObjects::location::{Location, LocationType}; use log::info; use serde::{Deserialize, Serialize}; use std::collections::{HashMap, HashSet}; -use std::fmt; -/// The basic struct used to represent components read from either Json or xml + +/// The basic struct used to represent automata read from either Json or xml. +/// It acts as the automata-representation in the code #[derive(Debug, Deserialize, Serialize, Clone, Eq, PartialEq)] -#[serde(into = "DummyComponent")] -pub struct Component { +#[serde(into = "DummyAutomaton")] +pub struct Automaton { pub name: String, #[serde( @@ -33,13 +26,13 @@ pub struct Component { pub edges: Vec, } -impl DeclarationProvider for Component { +impl DeclarationProvider for Automaton { fn get_declarations(&self) -> &Declarations { &self.declarations } } -impl Component { +impl Automaton { pub fn set_clock_indices(&mut self, indices: &mut ClockIndex) { self.declarations.set_clock_indices(*indices); *indices += self.declarations.get_clock_count(); @@ -162,12 +155,12 @@ impl Component { max_bounds } - /// Find [`Edge`] in the component given the edges `id`. + /// Find [`Edge`] in the automaton given the edges `id`. pub fn find_edge_from_id(&self, id: &str) -> Option<&Edge> { self.get_edges().iter().find(|e| e.id.contains(id)) } - /// Redoes the components Edge IDs by giving them new unique IDs based on their index. + /// Redoes the automatons Edge IDs by giving them new unique IDs based on their index. pub fn remake_edge_ids(&mut self) { // Give all edges a name for (index, edge) in self.get_mut_edges().iter_mut().enumerate() { @@ -204,7 +197,7 @@ impl Component { } }); info!( - "Removed Clock '{name}' (index {index}) has been removed from component {}", + "Removed Clock '{name}' (index {index}) has been removed from automaton {}", self.name ); // Should be changed in the future to be the information logger } @@ -228,7 +221,7 @@ impl Component { *index = global_index; // TODO: Maybe log the global clock name instead of index info!( - "Replaced Clock '{name}' (index {old}) with {global_index} in component {}", + "Replaced Clock '{name}' (index {old}) with {global_index} in automaton {}", self.name ); // Should be changed in the future to be the information logger } @@ -239,456 +232,6 @@ fn contain(channels: &[String], channel: &str) -> bool { channels.iter().any(|c| c == channel) } -/// FullState is a struct used for initial verification of consistency, and determinism as a state that also hols a dbm -/// This is done as the type used in refinement state pair assumes to sides of an operation -/// this should probably be refactored as it causes unnecessary confusion -#[derive(Clone, Debug)] -pub struct State { - pub decorated_locations: LocationTree, - zone_sentinel: Option, -} - -impl State { - pub fn create(decorated_locations: LocationTree, zone: OwnedFederation) -> Self { - State { - decorated_locations, - zone_sentinel: Some(zone), - } - } - - pub fn is_contained_in_list(&self, list: &[State]) -> bool { - list.iter().any(|s| self.is_subset_of(s)) - } - - pub fn from_location( - decorated_locations: LocationTree, - dimensions: ClockIndex, - ) -> Option { - let mut fed = OwnedFederation::init(dimensions); - - fed = decorated_locations.apply_invariants(fed); - if fed.is_empty() { - return None; - } - - Some(State { - decorated_locations, - zone_sentinel: Some(fed), - }) - } - - pub fn apply_invariants(&mut self) { - let fed = self.take_zone(); - let new_fed = self.decorated_locations.apply_invariants(fed); - self.set_zone(new_fed); - } - - pub fn zone_ref(&self) -> &OwnedFederation { - self.zone_sentinel.as_ref().unwrap() - } - - fn take_zone(&mut self) -> OwnedFederation { - self.zone_sentinel.take().unwrap() - } - - fn set_zone(&mut self, zone: OwnedFederation) { - self.zone_sentinel = Some(zone); - } - - pub fn update_zone(&mut self, update: impl FnOnce(OwnedFederation) -> OwnedFederation) { - let fed = self.take_zone(); - let new_fed = update(fed); - self.set_zone(new_fed); - } - - pub fn is_subset_of(&self, other: &Self) -> bool { - if self.decorated_locations != other.decorated_locations { - return false; - } - - self.zone_ref().subset_eq(other.zone_ref()) - } - - pub fn get_location(&self) -> &LocationTree { - &self.decorated_locations - } - - pub fn extrapolate_max_bounds(&mut self, system: &dyn TransitionSystem) { - let bounds = system.get_local_max_bounds(&self.decorated_locations); - self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) - } - - pub fn extrapolate_max_bounds_with_extra_bounds( - &mut self, - system: &dyn TransitionSystem, - extra_bounds: &Bounds, - ) { - let mut bounds = system.get_local_max_bounds(&self.decorated_locations); - bounds.add_bounds(extra_bounds); - self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) - } -} - -#[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq, Copy)] -pub enum LocationType { - Normal, - Initial, - Universal, - Inconsistent, - Any, -} - -impl LocationType { - pub fn combine(self, other: Self) -> Self { - match (self, other) { - (LocationType::Initial, LocationType::Initial) => LocationType::Initial, - _ => LocationType::Normal, - } - } -} - -#[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq)] -#[serde(into = "DummyLocation")] -pub struct Location { - pub id: String, - #[serde( - deserialize_with = "decode_invariant", - serialize_with = "encode_opt_boolexpr" - )] - pub invariant: Option, - #[serde( - deserialize_with = "decode_location_type", - serialize_with = "encode_location_type", - rename = "type" - )] - pub location_type: LocationType, - pub urgency: String, -} - -impl Location { - pub fn get_id(&self) -> &String { - &self.id - } - pub fn get_invariant(&self) -> &Option { - &self.invariant - } - pub fn get_location_type(&self) -> LocationType { - self.location_type - } - pub fn get_urgency(&self) -> &String { - &self.urgency - } -} - -#[derive(Debug, Deserialize, Serialize, Clone, Copy, PartialEq, Eq)] -pub enum SyncType { - Input, - Output, -} - -/// Represents a single transition from taking edges in multiple components -#[derive(Debug, Clone)] -pub struct Transition { - /// The ID of the transition, based on the edges it is created from. - pub id: TransitionID, - pub guard_zone: OwnedFederation, - pub target_locations: LocationTree, - pub updates: Vec, -} - -impl Transition { - /// Create a new transition not based on an edge with no identifier - pub fn new(target_locations: &LocationTree, dim: ClockIndex) -> Transition { - Transition { - id: TransitionID::None, - guard_zone: OwnedFederation::universe(dim), - target_locations: target_locations.clone(), - updates: vec![], - } - } - - pub fn from(comp: &Component, edge: &Edge, dim: ClockIndex) -> Transition { - //let (comp, edge) = edges; - - let target_loc_name = &edge.target_location; - let target_loc = comp.get_location_by_name(target_loc_name); - let target_locations = LocationTree::simple(target_loc, comp.get_declarations(), dim); - - let mut compiled_updates = vec![]; - if let Some(updates) = edge.get_update() { - compiled_updates.extend( - updates - .iter() - .map(|update| CompiledUpdate::compile(update, comp.get_declarations())), - ); - } - - Transition { - id: TransitionID::Simple(edge.id.clone()), - guard_zone: Transition::combine_edge_guards(&vec![(comp, edge)], dim), - target_locations, - updates: compiled_updates, - } - } - - pub fn use_transition(&self, state: &mut State) -> bool { - let mut zone = state.take_zone(); - zone = self.apply_guards(zone); - if !zone.is_empty() { - zone = self.apply_updates(zone).up(); - self.move_locations(&mut state.decorated_locations); - zone = state.decorated_locations.apply_invariants(zone); - if !zone.is_empty() { - state.set_zone(zone); - return true; - } - } - state.set_zone(zone); - false - } - - /// Returns the resulting [`State`] when using a transition in the given [`State`] - pub fn use_transition_alt(&self, state: &State) -> Option { - let mut state = state.to_owned(); - match self.use_transition(&mut state) { - true => Some(state), - false => None, - } - } - - pub fn combinations( - left: &Vec, - right: &Vec, - comp: CompositionType, - ) -> Vec { - let mut out: Vec = vec![]; - for l in left { - for r in right { - let target_locations = - LocationTree::compose(&l.target_locations, &r.target_locations, comp); - - let guard_zone = l.guard_zone.clone().intersection(&r.guard_zone); - - let mut updates = l.updates.clone(); - updates.append(&mut r.updates.clone()); - - out.push(Transition { - id: match comp { - CompositionType::Conjunction => TransitionID::Conjunction( - Box::new(l.id.clone()), - Box::new(r.id.clone()), - ), - CompositionType::Composition => TransitionID::Composition( - Box::new(l.id.clone()), - Box::new(r.id.clone()), - ), - _ => unreachable!("Invalid composition type {:?}", comp), - }, - guard_zone, - target_locations, - updates, - }); - } - } - - out - } - - pub fn apply_updates(&self, mut fed: OwnedFederation) -> OwnedFederation { - for update in &self.updates { - fed = update.apply(fed); - } - - fed - } - - pub fn inverse_apply_updates(&self, mut fed: OwnedFederation) -> OwnedFederation { - for update in &self.updates { - fed = update.apply_as_guard(fed); - } - for update in &self.updates { - fed = update.apply_as_free(fed); - } - - fed - } - - pub fn get_allowed_federation(&self) -> OwnedFederation { - let mut fed = match self.target_locations.get_invariants() { - Some(fed) => fed.clone(), - None => OwnedFederation::universe(self.guard_zone.dim()), - }; - fed = self.inverse_apply_updates(fed); - self.apply_guards(fed) - } - - pub fn apply_guards(&self, zone: OwnedFederation) -> OwnedFederation { - zone.intersection(&self.guard_zone) - } - - pub fn move_locations(&self, locations: &mut LocationTree) { - *locations = self.target_locations.clone(); - } - - pub fn combine_edge_guards( - edges: &Vec<(&Component, &Edge)>, - dim: ClockIndex, - ) -> OwnedFederation { - let mut fed = OwnedFederation::universe(dim); - for (comp, edge) in edges { - fed = edge.apply_guard(comp.get_declarations(), fed); - } - fed - } - - pub fn get_renamed_guard_expression( - &self, - naming: &HashMap, - ) -> Option { - BoolExpression::from_disjunction(&self.guard_zone.minimal_constraints(), naming) - } - - pub fn get_renamed_updates( - &self, - naming: &HashMap, - ) -> Option> { - let updates: Vec<_> = self.updates.iter().map(|u| u.as_update(naming)).collect(); - - if updates.is_empty() { - None - } else { - Some(updates) - } - } -} - -impl fmt::Display for Transition { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - f.write_fmt(format_args!( - "Transition{{{} to {} where {} [{}]}}", - self.guard_zone, - self.target_locations.id, - self.target_locations - .get_invariants() - .map(|f| format!("invariant is {}", f)) - .unwrap_or_else(|| "no invariant".to_string()), - self.updates - .iter() - .map(|u| u.to_string()) - .collect::>() - .join(", ") - ))?; - Ok(()) - } -} - -#[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq)] -#[serde(into = "DummyEdge")] -pub struct Edge { - /// Uniquely identifies the edge within its component - pub id: String, - #[serde(rename = "sourceLocation")] - pub source_location: String, - #[serde(rename = "targetLocation")] - pub target_location: String, - #[serde( - deserialize_with = "decode_sync_type", - serialize_with = "encode_sync_type", - rename = "status" - )] - pub sync_type: SyncType, - #[serde( - deserialize_with = "decode_guard", - serialize_with = "encode_opt_boolexpr" - )] - pub guard: Option, - #[serde( - deserialize_with = "decode_update", - serialize_with = "encode_opt_updates" - )] - pub update: Option>, - #[serde(deserialize_with = "decode_sync")] - pub sync: String, -} - -const TRUE: BoolExpression = BoolExpression::Bool(true); -impl fmt::Display for Edge { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - f.write_fmt(format_args!( - "Edge {{{}-({}{})->{}, Guard: {}, Update: {:?}}}", - self.source_location, - self.sync, - match self.sync_type { - SyncType::Input => "?", - SyncType::Output => "!", - }, - self.target_location, - self.guard.as_ref().unwrap_or(&TRUE), - self.update - ))?; - Ok(()) - } -} - -impl Edge { - pub fn apply_update( - &self, - decl: &Declarations, //Will eventually be mutable - mut fed: OwnedFederation, - ) -> OwnedFederation { - if let Some(updates) = self.get_update() { - for update in updates { - fed = update.compiled(decl).apply(fed); - } - } - - fed - } - - pub fn apply_guard(&self, decl: &Declarations, mut fed: OwnedFederation) -> OwnedFederation { - if let Some(guards) = self.get_guard() { - fed = apply_constraints_to_state(guards, decl, fed).expect("Failed to apply guard"); - }; - - fed - } - - pub fn get_source_location(&self) -> &String { - &self.source_location - } - - pub fn get_target_location(&self) -> &String { - &self.target_location - } - - pub fn get_sync_type(&self) -> &SyncType { - &self.sync_type - } - - pub fn get_guard(&self) -> &Option { - &self.guard - } - - pub fn get_update(&self) -> &Option> { - &self.update - } - - pub fn get_sync(&self) -> &String { - &self.sync - } - - pub fn get_update_clocks(&self) -> Vec<&str> { - let mut clock_vec = vec![]; - if let Some(updates) = self.get_update() { - for u in updates { - clock_vec.push(u.get_variable_name()) - } - } - - clock_vec - } -} - pub trait DeclarationProvider { fn get_declarations(&self) -> &Declarations; } diff --git a/src/ModelObjects/edge.rs b/src/ModelObjects/edge.rs new file mode 100644 index 00000000..b2e72150 --- /dev/null +++ b/src/ModelObjects/edge.rs @@ -0,0 +1,124 @@ +use crate::component::Declarations; +use crate::DataReader::parse_edge; +use crate::DataReader::serialization::{ + decode_guard, decode_sync, decode_sync_type, decode_update, DummyEdge, +}; +use crate::EdgeEval::constraint_applyer::apply_constraints_to_state; +use crate::ModelObjects::representations::BoolExpression; +use edbm::zones::OwnedFederation; +use serde::{Deserialize, Serialize}; +use std::fmt; + +#[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq)] +#[serde(into = "DummyEdge")] +pub struct Edge { + /// Uniquely identifies the edge within its component + pub id: String, + #[serde(rename = "sourceLocation")] + pub source_location: String, + #[serde(rename = "targetLocation")] + pub target_location: String, + #[serde( + deserialize_with = "decode_sync_type", + serialize_with = "encode_sync_type", + rename = "status" + )] + pub sync_type: SyncType, + #[serde( + deserialize_with = "decode_guard", + serialize_with = "encode_opt_boolexpr" + )] + pub guard: Option, + #[serde( + deserialize_with = "decode_update", + serialize_with = "encode_opt_updates" + )] + pub update: Option>, + #[serde(deserialize_with = "decode_sync")] + pub sync: String, +} + +impl fmt::Display for Edge { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + f.write_fmt(format_args!( + "Edge {{{}-({}{})->{}, Guard: {}, Update: {:?}}}", + self.source_location, + self.sync, + match self.sync_type { + SyncType::Input => "?", + SyncType::Output => "!", + }, + self.target_location, + self.guard.as_ref().unwrap_or(&TRUE), + self.update + ))?; + Ok(()) + } +} + +impl Edge { + pub fn apply_update( + &self, + decl: &Declarations, //Will eventually be mutable + mut fed: OwnedFederation, + ) -> OwnedFederation { + if let Some(updates) = self.get_update() { + for update in updates { + fed = update.compiled(decl).apply(fed); + } + } + + fed + } + + pub fn apply_guard(&self, decl: &Declarations, mut fed: OwnedFederation) -> OwnedFederation { + if let Some(guards) = self.get_guard() { + fed = apply_constraints_to_state(guards, decl, fed).expect("Failed to apply guard"); + }; + + fed + } + + pub fn get_source_location(&self) -> &String { + &self.source_location + } + + pub fn get_target_location(&self) -> &String { + &self.target_location + } + + pub fn get_sync_type(&self) -> &SyncType { + &self.sync_type + } + + pub fn get_guard(&self) -> &Option { + &self.guard + } + + pub fn get_update(&self) -> &Option> { + &self.update + } + + pub fn get_sync(&self) -> &String { + &self.sync + } + + pub fn get_update_clocks(&self) -> Vec<&str> { + let mut clock_vec = vec![]; + if let Some(updates) = self.get_update() { + for u in updates { + clock_vec.push(u.get_variable_name()) + } + } + + clock_vec + } +} + +#[derive(Debug, Deserialize, Serialize, Clone, Copy, PartialEq, Eq)] +pub enum SyncType { + Input, + Output, +} + +const TRUE: BoolExpression = BoolExpression::Bool(true); diff --git a/src/ModelObjects/location.rs b/src/ModelObjects/location.rs new file mode 100644 index 00000000..18577299 --- /dev/null +++ b/src/ModelObjects/location.rs @@ -0,0 +1,54 @@ +use crate::DataReader::serialization::{decode_invariant, decode_location_type, DummyLocation}; +use crate::ModelObjects::representations::BoolExpression; +use serde::{Deserialize, Serialize}; + +#[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq, Copy)] +pub enum LocationType { + Normal, + Initial, + Universal, + Inconsistent, + Any, +} + +impl LocationType { + pub fn combine(self, other: Self) -> Self { + match (self, other) { + (LocationType::Initial, LocationType::Initial) => LocationType::Initial, + _ => LocationType::Normal, + } + } +} + +#[derive(Debug, Deserialize, Serialize, Clone, PartialEq, Eq)] +#[serde(into = "DummyLocation")] +pub struct Location { + pub id: String, + #[serde( + deserialize_with = "decode_invariant", + serialize_with = "encode_opt_boolexpr" + )] + pub invariant: Option, + #[serde( + deserialize_with = "decode_location_type", + serialize_with = "encode_location_type", + rename = "type" + )] + pub location_type: LocationType, + pub urgency: String, +} + +impl Location { + pub fn get_id(&self) -> &String { + &self.id + } + pub fn get_invariant(&self) -> &Option { + &self.invariant + } + pub fn get_location_type(&self) -> LocationType { + self.location_type + } + pub fn get_urgency(&self) -> &String { + &self.urgency + } +} diff --git a/src/ModelObjects/mod.rs b/src/ModelObjects/mod.rs index b6790e28..ea287f60 100644 --- a/src/ModelObjects/mod.rs +++ b/src/ModelObjects/mod.rs @@ -1,5 +1,9 @@ pub mod component; +pub mod edge; +pub mod location; pub mod queries; pub mod representations; +pub mod state; pub mod statepair; pub mod system_declarations; +pub mod transition; diff --git a/src/ModelObjects/state.rs b/src/ModelObjects/state.rs new file mode 100644 index 00000000..b3679f28 --- /dev/null +++ b/src/ModelObjects/state.rs @@ -0,0 +1,94 @@ +use crate::TransitionSystems::{LocationTree, TransitionSystem}; +use edbm::util::bounds::Bounds; +use edbm::util::constraints::ClockIndex; +use edbm::zones::OwnedFederation; + +/// FullState is a struct used for initial verification of consistency, and determinism as a state that also hols a dbm +/// This is done as the type used in refinement state pair assumes to sides of an operation +/// this should probably be refactored as it causes unnecessary confusion +#[derive(Clone, Debug)] +pub struct State { + pub decorated_locations: LocationTree, + zone_sentinel: Option, +} + +impl State { + pub fn create(decorated_locations: LocationTree, zone: OwnedFederation) -> Self { + State { + decorated_locations, + zone_sentinel: Some(zone), + } + } + + pub fn is_contained_in_list(&self, list: &[State]) -> bool { + list.iter().any(|s| self.is_subset_of(s)) + } + + pub fn from_location( + decorated_locations: LocationTree, + dimensions: ClockIndex, + ) -> Option { + let mut fed = OwnedFederation::init(dimensions); + + fed = decorated_locations.apply_invariants(fed); + if fed.is_empty() { + return None; + } + + Some(State { + decorated_locations, + zone_sentinel: Some(fed), + }) + } + + pub fn apply_invariants(&mut self) { + let fed = self.take_zone(); + let new_fed = self.decorated_locations.apply_invariants(fed); + self.set_zone(new_fed); + } + + pub fn zone_ref(&self) -> &OwnedFederation { + self.zone_sentinel.as_ref().unwrap() + } + + pub(crate) fn take_zone(&mut self) -> OwnedFederation { + self.zone_sentinel.take().unwrap() + } + + pub(crate) fn set_zone(&mut self, zone: OwnedFederation) { + self.zone_sentinel = Some(zone); + } + + pub fn update_zone(&mut self, update: impl FnOnce(OwnedFederation) -> OwnedFederation) { + let fed = self.take_zone(); + let new_fed = update(fed); + self.set_zone(new_fed); + } + + pub fn is_subset_of(&self, other: &Self) -> bool { + if self.decorated_locations != other.decorated_locations { + return false; + } + + self.zone_ref().subset_eq(other.zone_ref()) + } + + pub fn get_location(&self) -> &LocationTree { + &self.decorated_locations + } + + pub fn extrapolate_max_bounds(&mut self, system: &dyn TransitionSystem) { + let bounds = system.get_local_max_bounds(&self.decorated_locations); + self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) + } + + pub fn extrapolate_max_bounds_with_extra_bounds( + &mut self, + system: &dyn TransitionSystem, + extra_bounds: &Bounds, + ) { + let mut bounds = system.get_local_max_bounds(&self.decorated_locations); + bounds.add_bounds(extra_bounds); + self.update_zone(|zone| zone.extrapolate_max_bounds(&bounds)) + } +} diff --git a/src/ModelObjects/system_declarations.rs b/src/ModelObjects/system_declarations.rs index d94bee51..512d1628 100644 --- a/src/ModelObjects/system_declarations.rs +++ b/src/ModelObjects/system_declarations.rs @@ -1,4 +1,4 @@ -use crate::ModelObjects::component::Component; +use crate::ModelObjects::component::Automaton; use log::debug; use serde::{Deserialize, Deserializer}; use std::collections::HashMap; @@ -18,33 +18,35 @@ impl SystemDeclarations { &mut self.declarations } - pub fn get_component_inputs(&self, comp_name: &str) -> Option<&Vec> { - self.get_declarations().get_input_actions().get(comp_name) + pub fn get_automaton_inputs(&self, automaton_name: &str) -> Option<&Vec> { + self.get_declarations() + .get_input_actions() + .get(automaton_name) } - pub fn add_component(&mut self, comp: &Component) { + pub fn add_automaton(&mut self, automaton: &Automaton) { self.declarations .input_actions - .insert(comp.get_name().clone(), comp.get_input_actions()); + .insert(automaton.get_name().clone(), automaton.get_input_actions()); self.declarations .output_actions - .insert(comp.get_name().clone(), comp.get_output_actions()); + .insert(automaton.get_name().clone(), automaton.get_output_actions()); } } #[derive(Debug, Deserialize, Clone)] pub struct SystemSpecification { - pub(crate) components: Vec, + pub(crate) automata: Vec, pub(crate) input_actions: HashMap>, pub(crate) output_actions: HashMap>, } impl SystemSpecification { - pub fn get_components(&self) -> &Vec { - &self.components + pub fn get_automata(&self) -> &Vec { + &self.automata } - pub fn get_mut_components(&mut self) -> &mut Vec { - &mut self.components + pub fn get_mut_automata(&mut self) -> &mut Vec { + &mut self.automata } pub fn get_input_actions(&self) -> &HashMap> { &self.input_actions @@ -70,9 +72,9 @@ where let decls: Vec = s.split('\n').map(|s| s.into()).collect(); let mut input_actions: HashMap> = HashMap::new(); let mut output_actions: HashMap> = HashMap::new(); - let mut components: Vec = vec![]; + let mut automata: Vec = vec![]; - let mut component_names: Vec = vec![]; + let mut automata_names: Vec = vec![]; for declaration in &decls { //skip comments @@ -82,29 +84,29 @@ where if !declaration.is_empty() { if first_run { - let component_decls = &declaration; - debug!("Comp decls: {component_decls}"); - component_names = component_decls.split(' ').map(|s| s.into()).collect(); + let automaton_decls = &declaration; + debug!("Automaton decls: {automaton_decls}"); + automata_names = automaton_decls.split(' ').map(|s| s.into()).collect(); - if component_names[0] == "system" { + if automata_names[0] == "system" { //do not include element 0 as that is the system keyword - for name in component_names.iter_mut().skip(1) { + for name in automata_names.iter_mut().skip(1) { let s = name.replace(',', ""); let s_cleaned = s.replace(';', ""); *name = s_cleaned.clone(); - components.push(s_cleaned); + automata.push(s_cleaned); } first_run = false; } else { - panic!("Unexpected format of system declarations. Missing system in beginning of {:?}", component_names) + panic!("Unexpected format of system declarations. Missing system in beginning of {:?}", automata_names) } } let split_string: Vec = declaration.split(' ').map(|s| s.into()).collect(); if split_string[0].as_str() == "IO" { - let component_name = split_string[1].clone(); + let automaton_name = split_string[1].clone(); - if component_names.contains(&component_name) { + if automata_names.contains(&automaton_name) { for split_str in split_string.iter().skip(2) { let s = split_str.replace('{', ""); let p = s.replace('}', ""); @@ -115,19 +117,19 @@ where } if action.ends_with('?') { let r = action.replace('?', ""); - if let Some(Channel_vec) = input_actions.get_mut(&component_name) { + if let Some(Channel_vec) = input_actions.get_mut(&automaton_name) { Channel_vec.push(r) } else { let Channel_vec = vec![r]; - input_actions.insert(component_name.clone(), Channel_vec); + input_actions.insert(automaton_name.clone(), Channel_vec); } } else if action.ends_with('!') { let r = action.replace('!', ""); - if let Some(Channel_vec) = output_actions.get_mut(&component_name) { + if let Some(Channel_vec) = output_actions.get_mut(&automaton_name) { Channel_vec.push(r.clone()) } else { let Channel_vec = vec![r.clone()]; - output_actions.insert(component_name.clone(), Channel_vec); + output_actions.insert(automaton_name.clone(), Channel_vec); } } else { panic!("Channel type not defined for Channel {:?}", action) @@ -135,13 +137,13 @@ where } } } else { - panic!("Was not able to find component name: {:?} in declared component names: {:?}", component_name, component_names) + panic!("Was not able to find automaton name: {:?} in declared automata names: {:?}", automaton_name, automata_names) } } } } Ok(SystemSpecification { - components, + automata, input_actions, output_actions, }) diff --git a/src/ModelObjects/transition.rs b/src/ModelObjects/transition.rs new file mode 100644 index 00000000..041af2a0 --- /dev/null +++ b/src/ModelObjects/transition.rs @@ -0,0 +1,207 @@ +use crate::component::{Automaton, DeclarationProvider}; +use crate::DataReader::parse_edge; +use crate::EdgeEval::updater::CompiledUpdate; +use crate::ModelObjects::edge::Edge; +use crate::ModelObjects::representations::BoolExpression; +use crate::ModelObjects::state::State; +use crate::TransitionSystems::{CompositionType, LocationTree, TransitionID}; +use edbm::util::constraints::ClockIndex; +use edbm::zones::OwnedFederation; +use std::collections::HashMap; +use std::fmt; + +/// Represents a single transition from taking edges in multiple components +#[derive(Debug, Clone)] +pub struct Transition { + /// The ID of the transition, based on the edges it is created from. + pub id: TransitionID, + pub guard_zone: OwnedFederation, + pub target_locations: LocationTree, + pub updates: Vec, +} + +impl Transition { + /// Create a new transition not based on an edge with no identifier + pub fn new(target_locations: &LocationTree, dim: ClockIndex) -> Transition { + Transition { + id: TransitionID::None, + guard_zone: OwnedFederation::universe(dim), + target_locations: target_locations.clone(), + updates: vec![], + } + } + + pub fn from(automaton: &Automaton, edge: &Edge, dim: ClockIndex) -> Transition { + //let (comp, edge) = edges; + + let target_loc_name = &edge.target_location; + let target_loc = automaton.get_location_by_name(target_loc_name); + let target_locations = LocationTree::simple(target_loc, automaton.get_declarations(), dim); + + let mut compiled_updates = vec![]; + if let Some(updates) = edge.get_update() { + compiled_updates.extend( + updates + .iter() + .map(|update| CompiledUpdate::compile(update, automaton.get_declarations())), + ); + } + + Transition { + id: TransitionID::Simple(edge.id.clone()), + guard_zone: Transition::combine_edge_guards(&vec![(automaton, edge)], dim), + target_locations, + updates: compiled_updates, + } + } + + pub fn use_transition(&self, state: &mut State) -> bool { + let mut zone = state.take_zone(); + zone = self.apply_guards(zone); + if !zone.is_empty() { + zone = self.apply_updates(zone).up(); + self.move_locations(&mut state.decorated_locations); + zone = state.decorated_locations.apply_invariants(zone); + if !zone.is_empty() { + state.set_zone(zone); + return true; + } + } + state.set_zone(zone); + false + } + + /// Returns the resulting [`State`] when using a transition in the given [`State`] + pub fn use_transition_alt(&self, state: &State) -> Option { + let mut state = state.to_owned(); + match self.use_transition(&mut state) { + true => Some(state), + false => None, + } + } + + pub fn combinations( + left: &Vec, + right: &Vec, + comp: CompositionType, + ) -> Vec { + let mut out: Vec = vec![]; + for l in left { + for r in right { + let target_locations = + LocationTree::compose(&l.target_locations, &r.target_locations, comp); + + let guard_zone = l.guard_zone.clone().intersection(&r.guard_zone); + + let mut updates = l.updates.clone(); + updates.append(&mut r.updates.clone()); + + out.push(Transition { + id: match comp { + CompositionType::Conjunction => TransitionID::Conjunction( + Box::new(l.id.clone()), + Box::new(r.id.clone()), + ), + CompositionType::Composition => TransitionID::Composition( + Box::new(l.id.clone()), + Box::new(r.id.clone()), + ), + _ => unreachable!("Invalid composition type {:?}", comp), + }, + guard_zone, + target_locations, + updates, + }); + } + } + + out + } + + pub fn apply_updates(&self, mut fed: OwnedFederation) -> OwnedFederation { + for update in &self.updates { + fed = update.apply(fed); + } + + fed + } + + pub fn inverse_apply_updates(&self, mut fed: OwnedFederation) -> OwnedFederation { + for update in &self.updates { + fed = update.apply_as_guard(fed); + } + for update in &self.updates { + fed = update.apply_as_free(fed); + } + + fed + } + + pub fn get_allowed_federation(&self) -> OwnedFederation { + let mut fed = match self.target_locations.get_invariants() { + Some(fed) => fed.clone(), + None => OwnedFederation::universe(self.guard_zone.dim()), + }; + fed = self.inverse_apply_updates(fed); + self.apply_guards(fed) + } + + pub fn apply_guards(&self, zone: OwnedFederation) -> OwnedFederation { + zone.intersection(&self.guard_zone) + } + + pub fn move_locations(&self, locations: &mut LocationTree) { + *locations = self.target_locations.clone(); + } + + pub fn combine_edge_guards( + edges: &Vec<(&Automaton, &Edge)>, + dim: ClockIndex, + ) -> OwnedFederation { + let mut fed = OwnedFederation::universe(dim); + for (comp, edge) in edges { + fed = edge.apply_guard(comp.get_declarations(), fed); + } + fed + } + + pub fn get_renamed_guard_expression( + &self, + naming: &HashMap, + ) -> Option { + BoolExpression::from_disjunction(&self.guard_zone.minimal_constraints(), naming) + } + + pub fn get_renamed_updates( + &self, + naming: &HashMap, + ) -> Option> { + let updates: Vec<_> = self.updates.iter().map(|u| u.as_update(naming)).collect(); + + if updates.is_empty() { + None + } else { + Some(updates) + } + } +} + +impl fmt::Display for Transition { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + f.write_fmt(format_args!( + "Transition{{{} to {} where {} [{}]}}", + self.guard_zone, + self.target_locations.id, + self.target_locations + .get_invariants() + .map(|f| format!("invariant is {}", f)) + .unwrap_or_else(|| "no invariant".to_string()), + self.updates + .iter() + .map(|u| u.to_string()) + .collect::>() + .join(", ") + ))?; + Ok(()) + } +} diff --git a/src/ProtobufServer/ecdar_requests/request_util.rs b/src/ProtobufServer/ecdar_requests/request_util.rs index 530f9b95..00f40579 100644 --- a/src/ProtobufServer/ecdar_requests/request_util.rs +++ b/src/ProtobufServer/ecdar_requests/request_util.rs @@ -3,45 +3,45 @@ use std::{collections::HashMap, sync::Arc}; use log::trace; use crate::{ - component::Component, - DataReader::component_loader::{parse_components_if_some, ComponentContainer, ModelCache}, + component::Automaton, + DataReader::component_loader::{parse_automata_if_some, AutomataContainer, ModelCache}, ProtobufServer::services::{Component as ProtoComponent, SimulationInfo}, System::input_enabler, TransitionSystems::{ - transition_system::component_loader_to_transition_system, TransitionSystemPtr, + transition_system::automata_loader_to_transition_system, TransitionSystemPtr, }, }; pub fn get_or_insert_model( model_cache: &mut ModelCache, user_id: i32, - components_hash: u32, + automata_hash: u32, proto_components: &[ProtoComponent], -) -> ComponentContainer { - match model_cache.get_model(user_id, components_hash) { +) -> AutomataContainer { + match model_cache.get_model(user_id, automata_hash) { Some(model) => model, None => { - let parsed_components: Vec = proto_components + let parsed_components: Vec = proto_components .iter() - .flat_map(parse_components_if_some) + .flat_map(parse_automata_if_some) .flatten() - .collect::>(); - let components = create_components(parsed_components); - model_cache.insert_model(user_id, components_hash, Arc::new(components)) + .collect::>(); + let automata = create_automata(parsed_components); + model_cache.insert_model(user_id, automata_hash, Arc::new(automata)) } } } -fn create_components(components: Vec) -> HashMap { - let mut comp_hashmap = HashMap::::new(); - for mut component in components { - trace!("Adding comp {} to container", component.get_name()); +fn create_automata(automata: Vec) -> HashMap { + let mut automata_hashmap = HashMap::::new(); + for mut automaton in automata { + trace!("Adding comp {} to container", automaton.get_name()); - let inputs: Vec<_> = component.get_input_actions(); - input_enabler::make_input_enabled(&mut component, &inputs); - comp_hashmap.insert(component.get_name().to_string(), component); + let inputs: Vec<_> = automaton.get_input_actions(); + input_enabler::make_input_enabled(&mut automaton, &inputs); + automata_hashmap.insert(automaton.get_name().to_string(), automaton); } - comp_hashmap + automata_hashmap } /// Borrows a [`SimulationInfo`] and returns the corresponding [`TransitionsSystemPtr`]. @@ -49,7 +49,7 @@ fn create_components(components: Vec) -> HashMap { /// # Panics /// If: /// - `simulation_info.components_info` is `None`. -/// - building the [`ComponentContainer`] fails. +/// - building the [`AutomataContainer`] fails. pub fn simulation_info_to_transition_system( simulation_info: &SimulationInfo, model_cache: &mut ModelCache, @@ -58,8 +58,8 @@ pub fn simulation_info_to_transition_system( let info = simulation_info.components_info.as_ref().unwrap(); let user_id = simulation_info.user_id; - let mut component_container = + let mut automata_container = get_or_insert_model(model_cache, user_id, info.components_hash, &info.components); - component_loader_to_transition_system(&mut component_container, &composition) + automata_loader_to_transition_system(&mut automata_container, &composition) } diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index 1f739d4f..06066547 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -1,6 +1,6 @@ use crate::extract_system_rep::ExecutableQueryError; use crate::DataReader::component_loader::ModelCache; -use crate::DataReader::json_writer::component_to_json; +use crate::DataReader::json_writer::automaton_to_json; use crate::DataReader::parse_queries; use crate::ModelObjects::queries::Query; use crate::ProtobufServer::ecdar_requests::request_util::get_or_insert_model; @@ -39,36 +39,36 @@ impl ConcreteEcdarBackend { let query = parse_query(&query_request)?; let user_id = query_request.user_id; - let mut component_container = get_or_insert_model( + let mut automata_container = get_or_insert_model( &mut model_cache, user_id, components_info.components_hash, proto_components, ); - component_container.set_settings(query_request.settings.unwrap_or(crate::DEFAULT_SETTINGS)); - - let out = - match extract_system_rep::create_executable_query(&query, &mut component_container) { - Ok(query) => { - let result = query.execute(); - Ok(QueryResponse { - query_id: query_request.query_id, - info: vec![], // TODO: Should be logs - result: Some(result.into()), - }) - } - Err(ExecutableQueryError::Custom(e)) => Err(Status::invalid_argument(format!( - "Creation of query failed: {}", - e - ))), - Err(ExecutableQueryError::SystemRecipeFailure(failure)) => { - Ok(QueryResponse { - query_id: query_request.query_id, - info: vec![], // TODO: Should be logs - result: Some(failure.into()), - }) - } - }; + automata_container.set_settings(query_request.settings.unwrap_or(crate::DEFAULT_SETTINGS)); + + let out = match extract_system_rep::create_executable_query(&query, &mut automata_container) + { + Ok(query) => { + let result = query.execute(); + Ok(QueryResponse { + query_id: query_request.query_id, + info: vec![], // TODO: Should be logs + result: Some(result.into()), + }) + } + Err(ExecutableQueryError::Custom(e)) => Err(Status::invalid_argument(format!( + "Creation of query failed: {}", + e + ))), + Err(ExecutableQueryError::SystemRecipeFailure(failure)) => { + Ok(QueryResponse { + query_id: query_request.query_id, + info: vec![], // TODO: Should be logs + result: Some(failure.into()), + }) + } + }; out } } @@ -97,8 +97,8 @@ impl From for ProtobufResult { QueryResult::Determinism(Err(fail)) => fail.into(), QueryResult::Reachability(Err(fail)) => fail.into(), - QueryResult::GetComponent(comp) => ProtobufResult::Component(ProtobufComponent { - rep: Some(Rep::Json(component_to_json(&comp))), + QueryResult::GetComponent(automaton) => ProtobufResult::Component(ProtobufComponent { + rep: Some(Rep::Json(automaton_to_json(&automaton))), }), QueryResult::RecipeFailure(recipe) => recipe.into(), diff --git a/src/ProtobufServer/proto_conversions.rs b/src/ProtobufServer/proto_conversions.rs index 7aafb720..84627791 100644 --- a/src/ProtobufServer/proto_conversions.rs +++ b/src/ProtobufServer/proto_conversions.rs @@ -12,7 +12,7 @@ use crate::ProtobufServer::services::{ }; use crate::System::query_failures::*; use crate::System::specifics::{ - SpecialLocation, SpecificClock, SpecificClockVar, SpecificComp, SpecificConjunction, + SpecialLocation, SpecificAutomaton, SpecificClock, SpecificClockVar, SpecificConjunction, SpecificConstraint, SpecificDecision, SpecificDisjunction, SpecificEdge, SpecificLocation, SpecificPath, SpecificState, }; @@ -45,10 +45,13 @@ impl From for LocationTree { }, ))), }, - SpecificLocation::ComponentLocation { comp, location_id } => LocationTree { + SpecificLocation::AutomatonLocation { + automaton, + location_id, + } => LocationTree { node_type: Some(NodeType::LeafLocation(LeafLocation { id: location_id, - component_instance: Some(comp.into()), + component_instance: Some(automaton.into()), })), }, SpecificLocation::SpecialLocation(kind) => LocationTree { @@ -79,8 +82,8 @@ impl From for SpecificLocation { SpecificLocation::BranchLocation(left, right, sys_type) } - NodeType::LeafLocation(leaf) => SpecificLocation::ComponentLocation { - comp: leaf.component_instance.unwrap().into(), + NodeType::LeafLocation(leaf) => SpecificLocation::AutomatonLocation { + automaton: leaf.component_instance.unwrap().into(), location_id: leaf.id, }, NodeType::SpecialLocation(special) => match special { @@ -92,20 +95,20 @@ impl From for SpecificLocation { } } -impl From for ProtoSpecificComponent { - fn from(comp: SpecificComp) -> Self { +impl From for ProtoSpecificComponent { + fn from(automaton: SpecificAutomaton) -> Self { ProtoSpecificComponent { - component_name: comp.name, - component_index: comp.id, + component_name: automaton.name, + component_index: automaton.id, } } } -impl From for SpecificComp { - fn from(comp: ProtoSpecificComponent) -> Self { - SpecificComp { - name: comp.component_name, - id: comp.component_index, +impl From for SpecificAutomaton { + fn from(automaton: ProtoSpecificComponent) -> Self { + SpecificAutomaton { + name: automaton.component_name, + id: automaton.component_index, } } } @@ -148,7 +151,7 @@ impl From for ProtoClock { SpecificClockVar::Zero => Self { clock: Some(ProtoClockEnum::ZeroClock(Default::default())), }, - SpecificClockVar::ComponentClock(clock) => Self { + SpecificClockVar::AutomatonClock(clock) => Self { clock: Some(ProtoClockEnum::ComponentClock(clock.into())), }, SpecificClockVar::SystemClock(clock_index) => Self { diff --git a/src/Simulation/decision.rs b/src/Simulation/decision.rs index b1fa6218..0025de8c 100644 --- a/src/Simulation/decision.rs +++ b/src/Simulation/decision.rs @@ -1,9 +1,8 @@ -use crate::{ - component::{State, Transition}, - TransitionSystems::TransitionSystemPtr, -}; +use crate::ModelObjects::state::State; +use crate::ModelObjects::transition::Transition; +use crate::TransitionSystems::TransitionSystemPtr; -/// Represent a decision in a any composition of components: In the current `state` [`State`] we have decided to take this `action` [`String`]. +/// Represent a decision in a any composition of automata: In the current `state` [`State`] we have decided to take this `action` [`String`]. #[derive(Debug, Clone)] pub struct Decision { pub state: State, diff --git a/src/Simulation/graph_layout.rs b/src/Simulation/graph_layout.rs index ce3c38ba..b578e5b6 100644 --- a/src/Simulation/graph_layout.rs +++ b/src/Simulation/graph_layout.rs @@ -1,4 +1,4 @@ -use crate::DataReader::serialization::DummyComponent; +use crate::DataReader::serialization::DummyAutomaton; use force_graph::{DefaultNodeIdx, ForceGraph, NodeData}; use log::info; use rand::Rng; @@ -10,14 +10,14 @@ use std::fs::File; use std::io::BufReader; use std::path::Path; -/// Configuration for component generation //TODO: use GRPC to set. +/// Configuration for automaton generation //TODO: use GRPC to set. #[derive(Debug, Deserialize)] struct Config { - /// Padding of sides of component + /// Padding of sides of automaton padding: f32, /// Square space needed for each location location_space: f32, - /// Maximal aspect ratio of the component + /// Maximal aspect ratio of the automaton max_ratio: f32, location_mass: f32, edge_mass: f32, @@ -62,7 +62,8 @@ struct Data { pub nail_number: usize, } -pub fn layout_dummy_component(comp: &mut DummyComponent) { +/// Automaton module +pub fn layout_dummy_automaton(comp: &mut DummyAutomaton) { let config = get_config(); // Compute the grid size @@ -206,7 +207,7 @@ pub fn layout_dummy_component(comp: &mut DummyComponent) { } }); - // Set the component shape + // Set the automaton shape comp.width = grid_size * ratio_x + config.padding; comp.height = grid_size * ratio_y + config.padding; @@ -214,7 +215,7 @@ pub fn layout_dummy_component(comp: &mut DummyComponent) { comp.x = -comp.width / 2.0; comp.y = -comp.height / 2.0; - // Choose a random color for the component + // Choose a random color for the automaton let color = rng.gen_range(0..10); comp.color = color.to_string(); diff --git a/src/System/executable_query.rs b/src/System/executable_query.rs index 95bfa2fe..80e1ad8b 100644 --- a/src/System/executable_query.rs +++ b/src/System/executable_query.rs @@ -1,8 +1,8 @@ -use crate::DataReader::component_loader::ComponentLoader; -use crate::ModelObjects::component::State; +use crate::AutomataLoader; +use crate::ModelObjects::state::State; use crate::System::reachability; use crate::System::refine; -use crate::System::save_component::combine_components; +use crate::System::save_component::combine_automata; use crate::TransitionSystems::TransitionSystemPtr; use super::query_failures::PathFailure; @@ -36,7 +36,7 @@ impl QueryResult { QueryResult::Determinism(Err(_)) => not_satisfied(query_str), QueryResult::GetComponent(_) => { - println!("{} -- Component succesfully created", query_str) + println!("{} -- Automaton successfully created", query_str) } QueryResult::CustomError(_) => println!("{} -- Failed", query_str), QueryResult::RecipeFailure(_) => not_satisfied(query_str), @@ -102,17 +102,17 @@ impl ExecutableQuery for ReachabilityExecutor { pub struct GetComponentExecutor<'a> { pub system: TransitionSystemPtr, pub comp_name: String, - pub component_loader: &'a mut dyn ComponentLoader, + pub automata_loader: &'a mut dyn AutomataLoader, } impl<'a> ExecutableQuery for GetComponentExecutor<'a> { fn execute(self: Box) -> QueryResult { - let mut comp = combine_components(&self.system, PruningStrategy::Reachable); + let mut comp = combine_automata(&self.system, PruningStrategy::Reachable); comp.name = self.comp_name; comp.remake_edge_ids(); - self.component_loader.save_component(comp.clone()); + self.automata_loader.save_automaton(comp.clone()); QueryResult::GetComponent(comp) } diff --git a/src/System/extract_state.rs b/src/System/extract_state.rs index 5740fac3..435e758a 100644 --- a/src/System/extract_state.rs +++ b/src/System/extract_state.rs @@ -2,8 +2,8 @@ use edbm::zones::OwnedFederation; use crate::extract_system_rep::SystemRecipe; use crate::EdgeEval::constraint_applyer::apply_constraints_to_state; -use crate::ModelObjects::component::State; use crate::ModelObjects::representations::{BoolExpression, QueryExpression}; +use crate::ModelObjects::state::State; use crate::TransitionSystems::{CompositionType, LocationID, LocationTree, TransitionSystemPtr}; use std::slice::Iter; @@ -88,15 +88,15 @@ fn build_location_tree( &build_location_tree(locations, right, right_system)?, )) } - SystemRecipe::Component(component) => match locations.next().unwrap().trim() { - // It is ensured .next() will not give a None, since the number of location is same as number of component. This is also being checked in validate_reachability_input function, that is called before get_state + SystemRecipe::Automaton(automaton) => match locations.next().unwrap().trim() { + // It is ensured .next() will not give a None, since the number of location is same as number of automata. This is also being checked in validate_reachability_input function, that is called before get_state "_" => Ok(LocationTree::build_any_location_tree()), str => system .get_location(&LocationID::Simple(str.to_string())) .ok_or(format!( - "Location {} does not exist in the component {}", + "Location {} does not exist in the automaton {}", str, - component.get_name() + automaton.get_name() )), }, } diff --git a/src/System/extract_system_rep.rs b/src/System/extract_system_rep.rs index 35c9ad51..f7f00564 100644 --- a/src/System/extract_system_rep.rs +++ b/src/System/extract_system_rep.rs @@ -1,5 +1,5 @@ -use crate::DataReader::component_loader::ComponentLoader; -use crate::ModelObjects::component::Component; +use crate::DataReader::component_loader::AutomataLoader; +use crate::ModelObjects::component::Automaton; use crate::ModelObjects::queries::Query; use crate::ModelObjects::representations::QueryExpression; use crate::System::executable_query::{ @@ -10,11 +10,11 @@ use crate::System::extract_state::get_state; use std::collections::HashMap; use crate::TransitionSystems::{ - CompiledComponent, Composition, Conjunction, Quotient, TransitionSystemPtr, + Composition, Conjunction, Quotient, SimpleTransitionSystem, TransitionSystemPtr, }; use super::query_failures::SystemRecipeFailure; -use crate::component::State; +use crate::ModelObjects::state::State; use crate::System::pruning; use crate::TransitionSystems::transition_system::ClockReductionInstruction; use edbm::util::constraints::ClockIndex; @@ -39,11 +39,11 @@ impl> From for ExecutableQueryError { } } -/// This function fetches the appropriate components based on the structure of the query and makes the enum structure match the query -/// this function also handles setting up the correct indices for clocks based on the amount of components in each system representation +/// This function fetches the appropriate automata based on the structure of the query and makes the enum structure match the query +/// this function also handles setting up the correct indices for clocks based on the amount of automata in each system representation pub fn create_executable_query<'a>( full_query: &Query, - component_loader: &'a mut (dyn ComponentLoader + 'static), + automata_loader: &'a mut (dyn AutomataLoader + 'static), ) -> Result, ExecutableQueryError> { let mut dim: ClockIndex = 0; @@ -52,21 +52,21 @@ pub fn create_executable_query<'a>( QueryExpression::Refinement(left_side, right_side) => { let mut quotient_index = None; - let mut left = get_system_recipe(left_side, component_loader, &mut dim, &mut quotient_index); - let mut right = get_system_recipe(right_side, component_loader, &mut dim, &mut quotient_index); + let mut left = get_system_recipe(left_side, automata_loader, &mut dim, &mut quotient_index); + let mut right = get_system_recipe(right_side, automata_loader, &mut dim, &mut quotient_index); - if !component_loader.get_settings().disable_clock_reduction { + if !automata_loader.get_settings().disable_clock_reduction { clock_reduction::clock_reduce(&mut left, Some(&mut right), &mut dim, quotient_index)?; } - let mut component_index = 0; + let mut automaton_index = 0; Ok(Box::new(RefinementExecutor { - sys1: left.compile_with_index(dim, &mut component_index)?, - sys2: right.compile_with_index(dim, &mut component_index)?, + sys1: left.compile_with_index(dim, &mut automaton_index)?, + sys2: right.compile_with_index(dim, &mut automaton_index)?, }))}, QueryExpression::Reachability(automata, start, end) => { - let machine = get_system_recipe(automata, component_loader, &mut dim, &mut None); + let machine = get_system_recipe(automata, automata_loader, &mut dim, &mut None); let transition_system = machine.clone().compile(dim)?; validate_reachability_input(&machine, end)?; @@ -98,12 +98,12 @@ pub fn create_executable_query<'a>( let mut quotient_index = None; let mut recipe = get_system_recipe( query_expression, - component_loader, + automata_loader, &mut dim, &mut quotient_index, ); - if !component_loader.get_settings().disable_clock_reduction { + if !automata_loader.get_settings().disable_clock_reduction { clock_reduction::clock_reduce(&mut recipe, None, &mut dim, quotient_index)?; } @@ -115,12 +115,12 @@ pub fn create_executable_query<'a>( let mut quotient_index = None; let mut recipe = get_system_recipe( query_expression, - component_loader, + automata_loader, &mut dim, &mut quotient_index, ); - if !component_loader.get_settings().disable_clock_reduction { + if !automata_loader.get_settings().disable_clock_reduction { clock_reduction::clock_reduce(&mut recipe, None, &mut dim, quotient_index)?; } @@ -133,12 +133,12 @@ pub fn create_executable_query<'a>( let mut quotient_index = None; let mut recipe = get_system_recipe( query_expression, - component_loader, + automata_loader, &mut dim, &mut quotient_index, ); - if !component_loader.get_settings().disable_clock_reduction { + if !automata_loader.get_settings().disable_clock_reduction { clock_reduction::clock_reduce(&mut recipe, None, &mut dim, quotient_index)?; } @@ -146,7 +146,7 @@ pub fn create_executable_query<'a>( GetComponentExecutor { system: recipe.compile(dim)?, comp_name: comp_name.clone(), - component_loader, + automata_loader, } )) }else{ @@ -159,11 +159,11 @@ pub fn create_executable_query<'a>( let mut quotient_index = None; let mut recipe = get_system_recipe( query_expression, - component_loader, + automata_loader, &mut dim, &mut quotient_index, ); - if !component_loader.get_settings().disable_clock_reduction { + if !automata_loader.get_settings().disable_clock_reduction { clock_reduction::clock_reduce(&mut recipe, None, &mut dim, quotient_index)?; } @@ -171,7 +171,7 @@ pub fn create_executable_query<'a>( GetComponentExecutor { system: pruning::prune_system(recipe.compile(dim)?, dim), comp_name: comp_name.clone(), - component_loader + automata_loader } )) }else{ @@ -192,67 +192,67 @@ pub enum SystemRecipe { Composition(Box, Box), Conjunction(Box, Box), Quotient(Box, Box, ClockIndex), - Component(Box), + Automaton(Box), } impl SystemRecipe { pub fn compile(self, dim: ClockIndex) -> Result> { - let mut component_index = 0; - self._compile(dim + 1, &mut component_index) + let mut automaton_index = 0; + self._compile(dim + 1, &mut automaton_index) } pub fn compile_with_index( self, dim: ClockIndex, - component_index: &mut u32, + automaton_index: &mut u32, ) -> Result> { - self._compile(dim + 1, component_index) + self._compile(dim + 1, automaton_index) } fn _compile( self, dim: ClockIndex, - component_index: &mut u32, + automaton_index: &mut u32, ) -> Result> { match self { SystemRecipe::Composition(left, right) => Composition::new_ts( - left._compile(dim, component_index)?, - right._compile(dim, component_index)?, + left._compile(dim, automaton_index)?, + right._compile(dim, automaton_index)?, dim, ), SystemRecipe::Conjunction(left, right) => Conjunction::new_ts( - left._compile(dim, component_index)?, - right._compile(dim, component_index)?, + left._compile(dim, automaton_index)?, + right._compile(dim, automaton_index)?, dim, ), SystemRecipe::Quotient(left, right, clock_index) => Quotient::new_ts( - left._compile(dim, component_index)?, - right._compile(dim, component_index)?, + left._compile(dim, automaton_index)?, + right._compile(dim, automaton_index)?, clock_index, dim, ), - SystemRecipe::Component(comp) => { - CompiledComponent::compile(*comp, dim, component_index) + SystemRecipe::Automaton(comp) => { + SimpleTransitionSystem::compile(*comp, dim, automaton_index) .map(|comp| comp as TransitionSystemPtr) } } } - /// Gets the number of `Components`s in the `SystemRecipe` - pub fn get_component_count(&self) -> usize { + /// Gets the number of [`Automaton`] in the [`SystemRecipe`] + pub fn get_automata_count(&self) -> usize { match self { SystemRecipe::Composition(left, right) | SystemRecipe::Conjunction(left, right) | SystemRecipe::Quotient(left, right, _) => { - left.get_component_count() + right.get_component_count() + left.get_automata_count() + right.get_automata_count() } - SystemRecipe::Component(_) => 1, + SystemRecipe::Automaton(_) => 1, } } ///Applies the clock-reduction fn reduce_clocks(&mut self, clock_instruction: Vec) { - let mut comps = self.get_components(); + let mut comps = self.get_automata(); for redundant in clock_instruction { match redundant { ClockReductionInstruction::RemoveClock { clock_index } => comps @@ -260,7 +260,7 @@ impl SystemRecipe { .find(|c| c.declarations.clocks.values().any(|ci| *ci == clock_index)) .unwrap_or_else(|| { panic!( - "A component could not be found for clock index {}", + "An automaton could not be found for clock index {}", clock_index ) }) @@ -275,17 +275,17 @@ impl SystemRecipe { } } - /// Gets all components in `SystemRecipe` - fn get_components(&mut self) -> Vec<&mut Component> { + /// Gets all automata in [`SystemRecipe`] + fn get_automata(&mut self) -> Vec<&mut Automaton> { match self { SystemRecipe::Composition(left, right) | SystemRecipe::Conjunction(left, right) | SystemRecipe::Quotient(left, right, _) => { - let mut o = left.get_components(); - o.extend(right.get_components()); + let mut o = left.get_automata(); + o.extend(right.get_automata()); o } - SystemRecipe::Component(c) => vec![c], + SystemRecipe::Automaton(c) => vec![c], } } fn change_quotient(&mut self, index: ClockIndex) { @@ -299,32 +299,32 @@ impl SystemRecipe { l.change_quotient(index); r.change_quotient(index); } - SystemRecipe::Component(_) => (), + SystemRecipe::Automaton(_) => (), } } } pub fn get_system_recipe( side: &QueryExpression, - component_loader: &mut dyn ComponentLoader, + automata_loader: &mut dyn AutomataLoader, clock_index: &mut ClockIndex, quotient_index: &mut Option, ) -> Box { match side { QueryExpression::Parentheses(expression) => { - get_system_recipe(expression, component_loader, clock_index, quotient_index) + get_system_recipe(expression, automata_loader, clock_index, quotient_index) } QueryExpression::Composition(left, right) => Box::new(SystemRecipe::Composition( - get_system_recipe(left, component_loader, clock_index, quotient_index), - get_system_recipe(right, component_loader, clock_index, quotient_index), + get_system_recipe(left, automata_loader, clock_index, quotient_index), + get_system_recipe(right, automata_loader, clock_index, quotient_index), )), QueryExpression::Conjunction(left, right) => Box::new(SystemRecipe::Conjunction( - get_system_recipe(left, component_loader, clock_index, quotient_index), - get_system_recipe(right, component_loader, clock_index, quotient_index), + get_system_recipe(left, automata_loader, clock_index, quotient_index), + get_system_recipe(right, automata_loader, clock_index, quotient_index), )), QueryExpression::Quotient(left, right) => { - let left = get_system_recipe(left, component_loader, clock_index, quotient_index); - let right = get_system_recipe(right, component_loader, clock_index, quotient_index); + let left = get_system_recipe(left, automata_loader, clock_index, quotient_index); + let right = get_system_recipe(right, automata_loader, clock_index, quotient_index); let q_index = match quotient_index { Some(q_i) => *q_i, @@ -340,14 +340,14 @@ pub fn get_system_recipe( Box::new(SystemRecipe::Quotient(left, right, q_index)) } QueryExpression::VarName(name) => { - let mut component = component_loader.get_component(name).clone(); - component.set_clock_indices(clock_index); - debug!("{} Clocks: {:?}", name, component.declarations.clocks); + let mut automaton = automata_loader.get_automaton(name).clone(); + automaton.set_clock_indices(clock_index); + debug!("{} Clocks: {:?}", name, automaton.declarations.clocks); - Box::new(SystemRecipe::Component(Box::new(component))) + Box::new(SystemRecipe::Automaton(Box::new(automaton))) } QueryExpression::SaveAs(comp, _) => { - get_system_recipe(comp, component_loader, clock_index, &mut None) + get_system_recipe(comp, automata_loader, clock_index, &mut None) } _ => panic!("Got unexpected query side: {:?}", side), } @@ -358,7 +358,7 @@ fn validate_reachability_input( state: &QueryExpression, ) -> Result<(), String> { if let QueryExpression::State(loc_names, _) = state { - if loc_names.len() != machine.get_component_count() { + if loc_names.len() != machine.get_automata_count() { return Err( "The number of automata does not match the number of locations".to_string(), ); @@ -402,7 +402,7 @@ pub(crate) mod clock_reduction { lhs.clone().compile(*dim)?.find_redundant_clocks(), rhs.clone().compile(*dim)?.find_redundant_clocks(), quotient_clock, - lhs.get_components() + lhs.get_automata() .iter() .flat_map(|c| c.declarations.clocks.values().cloned()) .max() @@ -418,7 +418,7 @@ pub(crate) mod clock_reduction { rhs.reduce_clocks(r_clocks); lhs.reduce_clocks(l_clocks); - compress_component_decls(lhs.get_components(), Some(rhs.get_components())); + compress_automata_decls(lhs.get_automata(), Some(rhs.get_automata())); if quotient_clock.is_some() { lhs.change_quotient(*dim); rhs.change_quotient(*dim); @@ -448,7 +448,7 @@ pub(crate) mod clock_reduction { .fold(0, |acc, c| acc + c.clocks_removed_count()); debug!("New dimension: {dim}"); sys.reduce_clocks(clocks); - compress_component_decls(sys.get_components(), None); + compress_automata_decls(sys.get_automata(), None); if quotient_clock.is_some() { sys.change_quotient(*dim); } @@ -493,10 +493,7 @@ pub(crate) mod clock_reduction { ) } - fn compress_component_decls( - mut comps: Vec<&mut Component>, - other: Option>, - ) { + fn compress_automata_decls(mut comps: Vec<&mut Automaton>, other: Option>) { let mut seen: HashMap = HashMap::new(); let mut l: Vec<&mut ClockIndex> = comps .iter_mut() diff --git a/src/System/input_enabler.rs b/src/System/input_enabler.rs index 1f8df17d..f47a6f22 100644 --- a/src/System/input_enabler.rs +++ b/src/System/input_enabler.rs @@ -1,24 +1,26 @@ +use crate::component::Automaton; +use crate::component::DeclarationProvider; +use crate::ModelObjects::edge::SyncType; use edbm::zones::OwnedFederation; use crate::EdgeEval::constraint_applyer; -use crate::ModelObjects::component; -use crate::ModelObjects::component::DeclarationProvider; +use crate::ModelObjects::edge::Edge; use crate::ModelObjects::representations::BoolExpression; -pub fn make_input_enabled(component: &mut component::Component, inputs: &[String]) { - let dimension = component.declarations.get_clock_count() + 1; - let mut new_edges: Vec = vec![]; - let input_edges = component +pub fn make_input_enabled(automaton: &mut Automaton, inputs: &[String]) { + let dimension = automaton.declarations.get_clock_count() + 1; + let mut new_edges: Vec = vec![]; + let input_edges = automaton .get_edges() .iter() - .filter(|edge| *edge.get_sync_type() == component::SyncType::Input); - for location in component.get_locations() { + .filter(|edge| *edge.get_sync_type() == SyncType::Input); + for location in automaton.get_locations() { let mut location_inv_zone = OwnedFederation::universe(dimension); if let Some(invariant) = location.get_invariant() { location_inv_zone = constraint_applyer::apply_constraints_to_state( invariant, - component.get_declarations(), + automaton.get_declarations(), location_inv_zone, ) .unwrap(); @@ -38,13 +40,13 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String for edge in specific_edges { let mut guard_zone = OwnedFederation::universe(dimension); - if let Some(target_invariant) = component + if let Some(target_invariant) = automaton .get_location_by_name(edge.get_target_location()) .get_invariant() { guard_zone = constraint_applyer::apply_constraints_to_state( target_invariant, - component.get_declarations(), + automaton.get_declarations(), guard_zone, ) .unwrap(); @@ -52,7 +54,7 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String if let Some(updates) = edge.get_update() { for update in updates { - let cu = update.compiled(component.get_declarations()); + let cu = update.compiled(automaton.get_declarations()); guard_zone = cu.apply_as_guard(guard_zone); guard_zone = cu.apply_as_free(guard_zone); } @@ -61,7 +63,7 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String if let Some(guard) = edge.get_guard() { guard_zone = constraint_applyer::apply_constraints_to_state( guard, - component.get_declarations(), + automaton.get_declarations(), guard_zone, ) .unwrap(); @@ -76,14 +78,14 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String continue; } - new_edges.push(component::Edge { + new_edges.push(Edge { id: format!("input_{}_{}", location.get_id(), input), source_location: location.get_id().to_string(), target_location: location.get_id().to_string(), - sync_type: component::SyncType::Input, + sync_type: SyncType::Input, guard: BoolExpression::from_disjunction( &result_federation.minimal_constraints(), - component.get_declarations().get_clocks(), + automaton.get_declarations().get_clocks(), ), update: None, sync: input.to_string(), @@ -91,5 +93,5 @@ pub fn make_input_enabled(component: &mut component::Component, inputs: &[String } } - component.add_edges(&mut new_edges); + automaton.add_edges(&mut new_edges); } diff --git a/src/System/local_consistency.rs b/src/System/local_consistency.rs index bbbfba8f..033bc9c6 100644 --- a/src/System/local_consistency.rs +++ b/src/System/local_consistency.rs @@ -1,7 +1,7 @@ use edbm::zones::OwnedFederation; use log::warn; -use crate::ModelObjects::component::State; +use crate::ModelObjects::state::State; use crate::System::query_failures::{ConsistencyFailure, DeterminismFailure}; use crate::TransitionSystems::TransitionSystem; diff --git a/src/System/pruning.rs b/src/System/pruning.rs index 47db8b18..a732abdf 100644 --- a/src/System/pruning.rs +++ b/src/System/pruning.rs @@ -3,14 +3,17 @@ use edbm::zones::OwnedFederation; use log::{debug, trace}; use crate::EdgeEval::constraint_applyer::apply_constraints_to_state; -use crate::ModelObjects::component::{ - Component, DeclarationProvider, Declarations, Edge, Location, SyncType, -}; +use crate::ModelObjects::component::Automaton; +use crate::ModelObjects::component::DeclarationProvider; +use crate::ModelObjects::component::Declarations; +use crate::ModelObjects::edge::SyncType; use crate::ModelObjects::representations::BoolExpression; -use crate::System::save_component::combine_components; +use crate::System::save_component::combine_automata; use crate::TransitionSystems::TransitionSystemPtr; -use crate::TransitionSystems::{CompiledComponent, LocationTree}; +use crate::TransitionSystems::{LocationTree, SimpleTransitionSystem}; +use crate::ModelObjects::edge::Edge; +use crate::ModelObjects::location::Location; use std::collections::{HashMap, HashSet}; use super::save_component::PruningStrategy; @@ -21,7 +24,7 @@ pub fn prune_system(ts: TransitionSystemPtr, dim: ClockIndex) -> TransitionSyste let inputs = ts.get_input_actions(); let outputs = ts.get_output_actions(); - let comp = combine_components(&ts, PruningStrategy::NoPruning); + let comp = combine_automata(&ts, PruningStrategy::NoPruning); let mut input_map: HashMap> = HashMap::new(); input_map.insert(comp.get_name().clone(), inputs.iter().cloned().collect()); @@ -32,7 +35,7 @@ pub fn prune_system(ts: TransitionSystemPtr, dim: ClockIndex) -> TransitionSyste } struct PruneContext { - comp: Component, + comp: Automaton, inconsistent_locs: Vec, inconsistent_parts: HashMap, passed_pairs: Vec<(String, OwnedFederation)>, @@ -79,17 +82,17 @@ impl PruneContext { } } - fn finish(self) -> (Component, HashMap) { + fn finish(self) -> (Automaton, HashMap) { (self.comp, self.inconsistent_parts) } } pub fn prune( - comp: &Component, + comp: &Automaton, dim: ClockIndex, inputs: HashSet, outputs: HashSet, -) -> Result, String> { +) -> Result, String> { let new_comp = comp.clone(); let inconsistent_locs: Vec<_> = new_comp .locations @@ -141,17 +144,17 @@ pub fn prune( add_inconsistent_parts_to_invariants(&mut new_comp, incons_parts, dim); debug!( - "Pruned component from {} edges to {} edges", + "Pruned automaton from {} edges to {} edges", comp.get_edges().len(), new_comp.get_edges().len() ); - CompiledComponent::compile_with_actions(new_comp, inputs, outputs, dim, 0) + SimpleTransitionSystem::compile_with_actions(new_comp, inputs, outputs, dim, 0) .map_err(|e| format!("Pruning failed: {}", e)) } fn add_inconsistent_parts_to_invariants( - comp: &mut Component, + comp: &mut Automaton, incons_parts: HashMap, dim: ClockIndex, ) { @@ -490,7 +493,7 @@ fn handle_output(edge: &Edge, context: &mut PruneContext) { fn is_immediately_inconsistent( location: &Location, - comp: &Component, + comp: &Automaton, dimensions: ClockIndex, ) -> bool { let loc = LocationTree::simple(location, &comp.declarations, dimensions); diff --git a/src/System/query_failures.rs b/src/System/query_failures.rs index 30f96535..1b2b20de 100644 --- a/src/System/query_failures.rs +++ b/src/System/query_failures.rs @@ -1,7 +1,8 @@ use std::{collections::HashSet, fmt}; +use crate::ModelObjects::state::State; use crate::{ - component::{Component, State}, + component::Automaton, ModelObjects::statepair::StatePair, TransitionSystems::{CompositionType, TransitionSystem, TransitionSystemPtr}, }; @@ -19,7 +20,7 @@ pub enum SystemType { Composition, /// A conjunction of two systems Conjunction, - /// A simple component, not composed with anything else + /// A simple automaton, not composed with anything else Simple, } @@ -44,12 +45,12 @@ impl fmt::Display for SystemType { Self::Refinement => write!(f, "Refinement"), Self::Composition => write!(f, "Composition"), Self::Conjunction => write!(f, "Conjunction"), - Self::Simple => write!(f, "Component"), + Self::Simple => write!(f, "Automaton"), } } } -/// Represents a system of components as a [String] `name` and the type of the highest level composition `sys_type` +/// Represents a system of automata as a [String] `name` and the type of the highest level composition `sys_type` #[derive(Clone, Debug, PartialEq, Eq)] pub struct System { pub name: String, @@ -88,7 +89,7 @@ impl System { } } -/// Represents a set of actions in a system of components. The system is represented by a [String] `system`, +/// Represents a set of actions in a system of automata. The system is represented by a [String] `system`, /// along with the `actions` and whether the actions are all inputs (`is_input`) or all outputs (`!is_input`). /// /// For representing a single action, see [Action]. @@ -111,7 +112,7 @@ impl fmt::Display for ActionSet { } } -/// Represents a single action in a system of components. The system is represented by a [String] `system`, +/// Represents a single action in a system of automata. The system is represented by a [String] `system`, /// along with the `action` and whether the action is an input (`is_input`). /// /// For representing a set of actions, see [ActionSet]. @@ -151,8 +152,8 @@ pub enum QueryResult { Consistency(ConsistencyResult), /// A determinism query returned a success or failure, see [DeterminismResult]. Determinism(DeterminismResult), - /// A get components query returned a new component. - GetComponent(Component), + /// A `get-component` query returned a new automaton. + GetComponent(Automaton), /// The query resulted in an unclassified error. CustomError(String), } diff --git a/src/System/reachability.rs b/src/System/reachability.rs index b25c158e..66e5e08e 100644 --- a/src/System/reachability.rs +++ b/src/System/reachability.rs @@ -3,7 +3,8 @@ use edbm::zones::OwnedFederation; use super::query_failures::PathFailure; use super::specifics::SpecificPath; -use crate::ModelObjects::component::{State, Transition}; +use crate::ModelObjects::state::State; +use crate::ModelObjects::transition::Transition; use crate::Simulation::decision::Decision; use crate::TransitionSystems::{LocationID, TransitionSystemPtr}; use std::collections::{HashMap, VecDeque}; diff --git a/src/System/refine.rs b/src/System/refine.rs index c8a0912c..60d1fb96 100644 --- a/src/System/refine.rs +++ b/src/System/refine.rs @@ -2,7 +2,7 @@ use edbm::zones::OwnedFederation; use log::{debug, info, log_enabled, trace, Level}; use crate::DataTypes::{PassedStateList, PassedStateListExt, WaitingStateList}; -use crate::ModelObjects::component::Transition; +use crate::ModelObjects::transition::Transition; use crate::ModelObjects::statepair::StatePair; use crate::System::query_failures::RefinementFailure; diff --git a/src/System/save_component.rs b/src/System/save_component.rs index 4f0b5986..4d6d8bed 100644 --- a/src/System/save_component.rs +++ b/src/System/save_component.rs @@ -1,5 +1,6 @@ -use crate::component::LocationType; -use crate::ModelObjects::component::{Component, Declarations, Edge, Location, SyncType}; +use crate::ModelObjects::component::{Automaton, Declarations}; +use crate::ModelObjects::edge::SyncType; +use crate::ModelObjects::location::{Location, LocationType}; use crate::ModelObjects::representations::BoolExpression; use crate::TransitionSystems::{LocationTree, TransitionSystemPtr}; use std::collections::HashMap; @@ -9,13 +10,11 @@ pub enum PruningStrategy { NoPruning, } +use crate::ModelObjects::edge::Edge; use edbm::util::constraints::ClockIndex; use PruningStrategy::*; -pub fn combine_components( - system: &TransitionSystemPtr, - reachability: PruningStrategy, -) -> Component { +pub fn combine_automata(system: &TransitionSystemPtr, reachability: PruningStrategy) -> Automaton { let mut location_trees = vec![]; let mut edges = vec![]; let clocks = get_clock_map(system); @@ -30,7 +29,7 @@ pub fn combine_components( let locations = get_locations_from_trees(&location_trees, &clocks); - Component { + Automaton { name: "".to_string(), declarations: Declarations { ints: HashMap::new(), diff --git a/src/System/specifics.rs b/src/System/specifics.rs index 877eabaa..ca0e9c3a 100644 --- a/src/System/specifics.rs +++ b/src/System/specifics.rs @@ -2,8 +2,8 @@ use std::{collections::HashMap, fmt}; use edbm::util::constraints::{ClockIndex, Conjunction, Constraint, Disjunction}; +use crate::ModelObjects::state::State; use crate::{ - component::State, ModelObjects::statepair::StatePair, Simulation::decision::Decision, TransitionSystems::{ @@ -98,34 +98,34 @@ impl SpecificPath { } } -/// Intermediate representation of a component instance. `id` is used to distinguish different instances of the same components in a system. +/// Intermediate representation of a automaton instance. `id` is used to distinguish different instances of the same automata in a system. #[derive(Clone, Debug, PartialEq, Eq, Hash)] -pub struct SpecificComp { +pub struct SpecificAutomaton { pub name: String, pub id: u32, } -impl SpecificComp { +impl SpecificAutomaton { pub fn new(name: String, id: u32) -> Self { Self { name, id } } } -/// Intermediate representation of an [edge](crate::ModelObjects::component::Edge) in a component instance. +/// Intermediate representation of an [edge](crate::ModelObjects::component::Edge) in an automaton instance. #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct SpecificEdge { - pub comp: SpecificComp, + pub comp: SpecificAutomaton, pub edge_id: String, } impl SpecificEdge { pub fn new( - component_name: impl Into, + automaton_name: impl Into, edge_id: impl Into, - component_id: u32, + automaton_id: u32, ) -> Self { Self { - comp: SpecificComp::new(component_name.into(), component_id), + comp: SpecificAutomaton::new(automaton_name.into(), automaton_id), edge_id: edge_id.into(), } } @@ -172,9 +172,9 @@ impl SpecificConjunction { pub enum SpecificClockVar { /// The zero clock. Zero, - /// A clock in a component instance. - ComponentClock(SpecificClock), - /// A clock without a component instance. E.g. a quotient clock. + /// A clock in an automaton instance. + AutomatonClock(SpecificClock), + /// A clock without an automaton instance. E.g. a quotient clock. SystemClock(ClockIndex), } @@ -196,7 +196,7 @@ impl SpecificConstraint { match clock { 0 => SpecificClockVar::Zero, _ => match sys.get(&clock) { - Some(c) => SpecificClockVar::ComponentClock(c.clone()), + Some(c) => SpecificClockVar::AutomatonClock(c.clone()), None => SpecificClockVar::SystemClock(clock), }, } @@ -219,12 +219,12 @@ pub struct SpecificState { } /// Intermediate representation of a [LocationID](crate::TransitionSystems::location_id::LocationID) in a system. -/// It is a binary tree with either [component](SpecificComp) locations or [special](SpecialLocation) locations at the leaves. +/// It is a binary tree with either [automaton](SpecificAutomaton) locations or [special](SpecialLocation) locations at the leaves. #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum SpecificLocation { - /// A location in a component instance. - ComponentLocation { - comp: SpecificComp, + /// A location in a automaton instance. + AutomatonLocation { + automaton: SpecificAutomaton, location_id: String, }, /// A branch with two child locations. @@ -235,12 +235,12 @@ pub enum SpecificLocation { impl SpecificLocation { pub fn new( - component_name: impl Into, + automaton_name: impl Into, location_id: impl Into, - component_id: u32, + automaton_id: u32, ) -> Self { - Self::ComponentLocation { - comp: SpecificComp::new(component_name.into(), component_id), + Self::AutomatonLocation { + automaton: SpecificAutomaton::new(automaton_name.into(), automaton_id), location_id: location_id.into(), } } @@ -259,7 +259,10 @@ impl SpecificLocation { impl fmt::Display for SpecificLocation { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - SpecificLocation::ComponentLocation { comp, location_id } => { + SpecificLocation::AutomatonLocation { + automaton: comp, + location_id, + } => { write!(f, "{}.{}", comp.name, location_id) } SpecificLocation::BranchLocation(left, right, op) => { @@ -329,15 +332,15 @@ impl fmt::Display for SpecificState { } } -/// Intermediate representation of a clock name in a specific [component instance](SpecificComp). +/// Intermediate representation of a clock name in a specific [automaton instance](SpecificAutomaton). #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct SpecificClock { pub name: String, - pub comp: SpecificComp, + pub comp: SpecificAutomaton, } impl SpecificClock { - pub fn new(name: String, comp: SpecificComp) -> Self { + pub fn new(name: String, comp: SpecificAutomaton) -> Self { Self { name, comp } } } @@ -355,7 +358,7 @@ pub fn specific_clock_comp_map(sys: &dyn TransitionSystem) -> HashMap { let info = infos.info(); - SpecificLocation::ComponentLocation { - comp: SpecificComp::new(info.name.clone(), info.id), + SpecificLocation::AutomatonLocation { + automaton: SpecificAutomaton::new(info.name.clone(), info.id), location_id: loc_id.clone(), } } diff --git a/src/TransitionSystems/common.rs b/src/TransitionSystems/common.rs index e8ac296a..bd176f52 100644 --- a/src/TransitionSystems/common.rs +++ b/src/TransitionSystems/common.rs @@ -7,8 +7,10 @@ use edbm::{ }; use log::warn; +use crate::ModelObjects::state::State; +use crate::ModelObjects::transition::Transition; use crate::{ - ModelObjects::component::{Declarations, State, Transition}, + ModelObjects::component::Declarations, System::{query_failures::DeterminismResult, specifics::SpecificLocation}, }; use crate::{System::query_failures::ConsistencyResult, TransitionSystems::CompositionType}; diff --git a/src/TransitionSystems/compiled_component.rs b/src/TransitionSystems/compiled_component.rs index 1ef519d4..66fc152a 100644 --- a/src/TransitionSystems/compiled_component.rs +++ b/src/TransitionSystems/compiled_component.rs @@ -1,6 +1,8 @@ -use crate::ModelObjects::component::{ - Component, DeclarationProvider, Declarations, State, Transition, -}; +use crate::ModelObjects::component::Automaton; +use crate::ModelObjects::component::DeclarationProvider; +use crate::ModelObjects::component::Declarations; +use crate::ModelObjects::state::State; +use crate::ModelObjects::transition::Transition; use crate::System::local_consistency::{self}; use crate::System::query_failures::{ ActionFailure, ConsistencyResult, DeterminismResult, SystemRecipeFailure, @@ -27,7 +29,7 @@ pub struct ComponentInfo { } #[derive(Clone)] -pub struct CompiledComponent { +pub struct SimpleTransitionSystem { inputs: HashSet, outputs: HashSet, locations: HashMap, @@ -37,24 +39,24 @@ pub struct CompiledComponent { dim: ClockIndex, } -impl CompiledComponent { +impl SimpleTransitionSystem { pub fn compile_with_actions( - component: Component, + automaton: Automaton, inputs: HashSet, outputs: HashSet, dim: ClockIndex, id: u32, ) -> Result, Box> { if !inputs.is_disjoint(&outputs) { - ActionFailure::not_disjoint_IO(&component.name, inputs.clone(), outputs.clone()) - .map_err(|e| e.to_simple_failure(&component.name))?; + ActionFailure::not_disjoint_IO(&automaton.name, inputs.clone(), outputs.clone()) + .map_err(|e| e.to_simple_failure(&automaton.name))?; } - let locations: HashMap = component + let locations: HashMap = automaton .get_locations() .iter() .map(|loc| { - let loc = LocationTree::simple(loc, component.get_declarations(), dim); + let loc = LocationTree::simple(loc, automaton.get_declarations(), dim); (loc.id.clone(), loc) }) .collect(); @@ -62,9 +64,9 @@ impl CompiledComponent { let mut location_edges: HashMap> = locations.keys().map(|k| (k.clone(), vec![])).collect(); - for edge in component.get_edges() { + for edge in automaton.get_edges() { let id = LocationID::Simple(edge.source_location.clone()); - let transition = Transition::from(&component, edge, dim); + let transition = Transition::from(&automaton, edge, dim); location_edges .get_mut(&id) .unwrap() @@ -73,8 +75,8 @@ impl CompiledComponent { let initial_location = locations.values().find(|loc| loc.is_initial()).cloned(); - let max_bounds = component.get_max_bounds(dim); - Ok(Box::new(CompiledComponent { + let max_bounds = automaton.get_max_bounds(dim); + Ok(Box::new(SimpleTransitionSystem { inputs, outputs, locations, @@ -82,8 +84,8 @@ impl CompiledComponent { initial_location, dim, comp_info: ComponentInfo { - name: component.name, - declarations: component.declarations, + name: automaton.name, + declarations: automaton.declarations, max_bounds, id, }, @@ -91,15 +93,15 @@ impl CompiledComponent { } pub fn compile( - component: Component, + automaton: Automaton, dim: ClockIndex, - component_index: &mut u32, + automaton_index: &mut u32, ) -> Result, Box> { - let inputs = HashSet::from_iter(component.get_input_actions()); - let outputs = HashSet::from_iter(component.get_output_actions()); - let index = *component_index; - *component_index += 1; - Self::compile_with_actions(component, inputs, outputs, dim, index) + let inputs = HashSet::from_iter(automaton.get_input_actions()); + let outputs = HashSet::from_iter(automaton.get_output_actions()); + let index = *automaton_index; + *automaton_index += 1; + Self::compile_with_actions(automaton, inputs, outputs, dim, index) } fn _comp_info(&self) -> &ComponentInfo { @@ -107,7 +109,7 @@ impl CompiledComponent { } } -impl TransitionSystem for CompiledComponent { +impl TransitionSystem for SimpleTransitionSystem { fn get_local_max_bounds(&self, loc: &LocationTree) -> Bounds { if loc.is_universal() || loc.is_inconsistent() { Bounds::new(self.get_dim()) @@ -198,7 +200,7 @@ impl TransitionSystem for CompiledComponent { self.locations.get(id).cloned() } - fn component_names(&self) -> Vec<&str> { + fn automata_names(&self) -> Vec<&str> { vec![&self.comp_info.name] } @@ -212,20 +214,23 @@ impl TransitionSystem for CompiledComponent { fn construct_location_tree(&self, target: SpecificLocation) -> Result { match target { - SpecificLocation::ComponentLocation { comp, location_id } => { + SpecificLocation::AutomatonLocation { + automaton: comp, + location_id, + } => { assert_eq!(comp.name, self.comp_info.name); self.get_all_locations() .into_iter() .find(|loc| loc.id == LocationID::Simple(location_id.clone())) .ok_or_else(|| { format!( - "Could not find location {} in component {}", + "Could not find location {} in automaton {}", location_id, self.comp_info.name ) }) } SpecificLocation::BranchLocation(_, _, _) | SpecificLocation::SpecialLocation(_) => { - unreachable!("Should not happen at the level of a component.") + unreachable!("Should not happen at the level of a automaton.") } } } diff --git a/src/TransitionSystems/composition.rs b/src/TransitionSystems/composition.rs index 982a88fe..013c0d83 100644 --- a/src/TransitionSystems/composition.rs +++ b/src/TransitionSystems/composition.rs @@ -1,6 +1,6 @@ use edbm::util::constraints::ClockIndex; -use crate::ModelObjects::component::Transition; +use crate::ModelObjects::transition::Transition; use crate::System::query_failures::{ActionFailure, SystemRecipeFailure}; use crate::TransitionSystems::{LocationTree, TransitionSystem, TransitionSystemPtr}; use std::collections::hash_set::HashSet; diff --git a/src/TransitionSystems/conjunction.rs b/src/TransitionSystems/conjunction.rs index 10ffb1f7..a4d36ac8 100644 --- a/src/TransitionSystems/conjunction.rs +++ b/src/TransitionSystems/conjunction.rs @@ -1,6 +1,6 @@ use edbm::util::constraints::ClockIndex; -use crate::ModelObjects::component::Transition; +use crate::ModelObjects::transition::Transition; use crate::System::local_consistency; use crate::System::query_failures::{ActionFailure, ConsistencyResult, SystemRecipeFailure}; use crate::TransitionSystems::{ diff --git a/src/TransitionSystems/location_tree.rs b/src/TransitionSystems/location_tree.rs index bfdfb678..1776e98a 100644 --- a/src/TransitionSystems/location_tree.rs +++ b/src/TransitionSystems/location_tree.rs @@ -1,8 +1,8 @@ use edbm::{util::constraints::ClockIndex, zones::OwnedFederation}; +use crate::ModelObjects::location::{Location, LocationType}; use crate::{ - EdgeEval::constraint_applyer::apply_constraints_to_state, - ModelObjects::component::{Declarations, Location, LocationType}, + EdgeEval::constraint_applyer::apply_constraints_to_state, ModelObjects::component::Declarations, }; use super::LocationID; diff --git a/src/TransitionSystems/mod.rs b/src/TransitionSystems/mod.rs index f2d2552f..47b4e2ee 100644 --- a/src/TransitionSystems/mod.rs +++ b/src/TransitionSystems/mod.rs @@ -9,7 +9,7 @@ mod quotient; mod transition_id; pub mod transition_system; -pub use compiled_component::{CompiledComponent, ComponentInfo}; +pub use compiled_component::{ComponentInfo, SimpleTransitionSystem}; pub use composition::Composition; pub use conjunction::Conjunction; pub use location_id::LocationID; diff --git a/src/TransitionSystems/quotient.rs b/src/TransitionSystems/quotient.rs index dc9aba16..ee1d7d8a 100644 --- a/src/TransitionSystems/quotient.rs +++ b/src/TransitionSystems/quotient.rs @@ -4,13 +4,14 @@ use log::debug; use crate::EdgeEval::updater::CompiledUpdate; use crate::ModelObjects::component::Declarations; -use crate::ModelObjects::component::{State, Transition}; +use crate::ModelObjects::transition::Transition; use crate::System::query_failures::{ ActionFailure, ConsistencyResult, DeterminismResult, SystemRecipeFailure, }; use crate::System::specifics::{SpecialLocation, SpecificLocation}; use edbm::util::bounds::Bounds; +use crate::ModelObjects::state::State; use crate::TransitionSystems::{LocationTree, TransitionID, TransitionSystem, TransitionSystemPtr}; use std::collections::hash_set::HashSet; use std::vec; @@ -397,7 +398,7 @@ impl TransitionSystem for Quotient { SpecificLocation::SpecialLocation(SpecialLocation::Error) => { Ok(self.inconsistent_location.clone()) } - SpecificLocation::ComponentLocation { .. } => unreachable!("Should not occur"), + SpecificLocation::AutomatonLocation { .. } => unreachable!("Should not occur"), } } } diff --git a/src/TransitionSystems/transition_id.rs b/src/TransitionSystems/transition_id.rs index eb8ad89e..c8bfad5a 100644 --- a/src/TransitionSystems/transition_id.rs +++ b/src/TransitionSystems/transition_id.rs @@ -13,7 +13,7 @@ pub enum TransitionID { } impl TransitionID { - /// Returns a vector of transitionIDs for all components involved in the transition + /// Returns a vector of transitionIDs for all automata involved in the transition /// For example /// ``` /// use crate::reveaal::TransitionSystems::TransitionID; @@ -23,7 +23,7 @@ impl TransitionID { /// let leaves = id.get_leaves(); /// assert_eq!(leaves, vec![vec![TransitionID::Simple("a".to_string())], vec![TransitionID::Simple("b".to_string())]]) /// ``` - /// Leaves will be {{a}, {b}}, as a is from the first component and b is from the second component + /// Leaves will be `{{a}, {b}}`, as `a` is from the first automaton and `b` is from the second automaton pub fn get_leaves(&self) -> Vec> { let mut result = Vec::new(); self.get_leaves_helper(&mut result, 0); @@ -61,7 +61,7 @@ impl TransitionID { } } - /// Takes a path of TransitionIDs, and splits them into seperate paths for each component + /// Takes a path of TransitionIDs, and splits them into seperate paths for each automaton /// For example /// ``` /// use crate::reveaal::TransitionSystems::TransitionID; @@ -74,8 +74,8 @@ impl TransitionID { /// Box::new(TransitionID::Simple("c".to_string())), /// Box::new(TransitionID::Simple("d".to_string()))) /// ]; - /// let component_paths = TransitionID::split_into_component_lists(&path); - /// assert_eq!(component_paths, Ok( + /// let automta_paths = TransitionID::split_into_automata_lists(&path); + /// assert_eq!(automta_paths, Ok( /// vec![ /// vec![ /// vec![TransitionID::Simple("a".to_string())], @@ -84,8 +84,8 @@ impl TransitionID { /// vec![TransitionID::Simple("b".to_string())], /// vec![TransitionID::Simple("d".to_string())]]])); /// ``` - /// component_paths will be {{a, c}, {b, d}}, representing the paths for the two components - pub fn split_into_component_lists( + /// `automata_paths` will be `{{a, c}, {b, d}}`, representing the paths for the two automata + pub fn split_into_automata_lists( path: &Vec, ) -> Result>>, String> { if path.is_empty() { @@ -97,11 +97,11 @@ impl TransitionID { for transitionID in path { let leaves = transitionID.get_leaves(); - for (componentIndex, transition) in leaves.iter().enumerate() { + for (automaton_index, transition) in leaves.iter().enumerate() { if leaves.len() != amount { - return Err(format!("Could not split into components because first transition has {} components but {:?} has {} components", amount, leaves, leaves.len())); + return Err(format!("Could not split into automata because first transition has {} automata but {:?} has {} automata", amount, leaves, leaves.len())); } - paths[componentIndex].push( + paths[automaton_index].push( transition .iter() .cloned() diff --git a/src/TransitionSystems/transition_system.rs b/src/TransitionSystems/transition_system.rs index f0abebfa..be4b2f15 100644 --- a/src/TransitionSystems/transition_system.rs +++ b/src/TransitionSystems/transition_system.rs @@ -2,15 +2,17 @@ use super::ComponentInfo; use super::{CompositionType, LocationID, LocationTree}; use crate::DataReader::parse_queries::Rule; use crate::EdgeEval::updater::CompiledUpdate; +use crate::ModelObjects::state::State; +use crate::ModelObjects::transition::Transition; use crate::System::query_failures::{ConsistencyResult, DeterminismResult}; use crate::System::specifics::SpecificLocation; use crate::{ - component::Component, + component::Automaton, extract_system_rep::get_system_recipe, parse_queries::{build_expression_from_pair, QueryParser}, - ComponentLoader, - DataReader::component_loader::ComponentContainer, - ModelObjects::component::{Declarations, State, Transition}, + AutomataLoader, + DataReader::component_loader::AutomataContainer, + ModelObjects::component::Declarations, }; use dyn_clone::{clone_trait_object, DynClone}; use edbm::util::{bounds::Bounds, constraints::ClockIndex}; @@ -166,15 +168,15 @@ pub trait TransitionSystem: DynClone { format!("({} {} {})", left.to_string(), comp, right.to_string()) } - /// Returns a [`Vec`] of all component names in a given [`TransitionSystem`]. - fn component_names(&self) -> Vec<&str> { + /// Returns a [`Vec`] of all automata names in a given [`TransitionSystem`]. + fn automata_names(&self) -> Vec<&str> { let children = self.get_children(); let left_child = children.0; let right_child = children.1; left_child - .component_names() + .automata_names() .into_iter() - .chain(right_child.component_names().into_iter()) + .chain(right_child.automata_names().into_iter()) .collect() } @@ -251,18 +253,18 @@ pub trait TransitionSystem: DynClone { fn construct_location_tree(&self, target: SpecificLocation) -> Result; } -/// Returns a [`TransitionSystemPtr`] equivalent to a `composition` of some `components`. -pub fn components_to_transition_system( - components: Vec, +/// Returns a [`TransitionSystemPtr`] equivalent to a `composition` of some automata. +pub fn automata_to_transition_system( + automata: Vec, composition: &str, ) -> TransitionSystemPtr { - let mut component_container = ComponentContainer::from_components(components); - component_loader_to_transition_system(&mut component_container, composition) + let mut automata_container = AutomataContainer::from_automata(automata); + automata_loader_to_transition_system(&mut automata_container, composition) } -/// Returns a [`TransitionSystemPtr`] equivalent to a `composition` of some components in a [`ComponentLoader`]. -pub fn component_loader_to_transition_system( - loader: &mut dyn ComponentLoader, +/// Returns a [`TransitionSystemPtr`] equivalent to a `composition` of some automata in a [`AutomataLoader`]. +pub fn automata_loader_to_transition_system( + loader: &mut dyn AutomataLoader, composition: &str, ) -> TransitionSystemPtr { let mut dimension = 0; diff --git a/src/lib.rs b/src/lib.rs index e8a6c57c..b915f642 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -11,7 +11,7 @@ pub mod logging; pub mod tests; pub use crate::DataReader::component_loader::{ - ComponentLoader, JsonProjectLoader, ProjectLoader, XmlProjectLoader, + AutomataLoader, JsonProjectLoader, ProjectLoader, XmlProjectLoader, }; pub use crate::DataReader::{parse_queries, xml_parser}; pub use crate::ModelObjects::queries::Query; diff --git a/src/main.rs b/src/main.rs index af0c90d4..47935937 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,7 +5,7 @@ use reveaal::System::query_failures::QueryResult; use reveaal::ProtobufServer::services::query_request::Settings; use reveaal::{ - extract_system_rep, parse_queries, start_grpc_server_with_tokio, xml_parser, ComponentLoader, + extract_system_rep, parse_queries, start_grpc_server_with_tokio, xml_parser, AutomataLoader, JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, }; use std::env; @@ -60,7 +60,7 @@ fn start_using_cli(matches: &clap::ArgMatches) { } } -fn parse_args(matches: &clap::ArgMatches) -> (Box, Vec) { +fn parse_args(matches: &clap::ArgMatches) -> (Box, Vec) { let folder_path = matches.value_of("folder").unwrap_or(""); let query = matches.value_of("query").unwrap_or(""); let settings = Settings { diff --git a/src/tests/ClockReduction/clock_removal_test.rs b/src/tests/ClockReduction/clock_removal_test.rs index a1872d7a..ae5344db 100644 --- a/src/tests/ClockReduction/clock_removal_test.rs +++ b/src/tests/ClockReduction/clock_removal_test.rs @@ -1,10 +1,10 @@ #[cfg(test)] pub mod clock_removal_tests { - use crate::component::Component; + use crate::component::Automaton; use crate::extract_system_rep::{clock_reduction, SystemRecipe}; use crate::tests::refinement::Helper::json_run_query; - use crate::DataReader::json_reader::read_json_component; - use crate::TransitionSystems::{CompiledComponent, TransitionSystem}; + use crate::DataReader::json_reader::read_json_automaton; + use crate::TransitionSystems::{SimpleTransitionSystem, TransitionSystem}; use std::collections::HashSet; #[test] @@ -14,7 +14,7 @@ pub mod clock_removal_tests { check_declarations_unused_clocks_are_removed("Component3", "c"); } - impl Component { + impl Automaton { fn fit_decls(&mut self, index: edbm::util::constraints::ClockIndex) { self.declarations .clocks @@ -25,7 +25,7 @@ pub mod clock_removal_tests { } fn check_declarations_unused_clocks_are_removed(component_name: &str, clock: &str) { - let mut component = read_json_component( + let mut component = read_json_automaton( "samples/json/ClockReductionTest/UnusedClock", component_name, ); @@ -38,7 +38,7 @@ pub mod clock_removal_tests { component.remove_clock(clock_index); component.fit_decls(clock_index); - let clock_reduced_compiled_component = CompiledComponent::compile( + let clock_reduced_compiled_component = SimpleTransitionSystem::compile( component.clone(), component.declarations.clocks.len() + 1, &mut 0, @@ -52,7 +52,7 @@ pub mod clock_removal_tests { #[test] fn test_check_declarations_duplicated_clocks_are_removed() { - let mut component = read_json_component( + let mut component = read_json_automaton( "samples/json/ClockReductionTest/RedundantClocks", "Component1", ); @@ -66,7 +66,7 @@ pub mod clock_removal_tests { component.replace_clock(*clock_1_index, &duplicate_clocks_index); - let clock_reduced_compiled_component = CompiledComponent::compile( + let clock_reduced_compiled_component = SimpleTransitionSystem::compile( component.clone(), component.declarations.clocks.len() + 1, &mut 0, @@ -84,7 +84,7 @@ pub mod clock_removal_tests { fn test_no_used_clock() { const PATH: &str = "samples/json/AG"; - let comp = read_json_component(PATH, "A"); + let comp = read_json_automaton(PATH, "A"); let mut dim = comp.declarations.clocks.len(); assert_eq!( @@ -92,7 +92,7 @@ pub mod clock_removal_tests { "As of writing these tests, this component has 4 unused clocks" ); - let recipe = SystemRecipe::Component(Box::from(comp)); + let recipe = SystemRecipe::Automaton(Box::from(comp)); clock_reduction::clock_reduce(&mut Box::from(recipe), None, &mut dim, None).unwrap(); assert_eq!(dim, 0, "After removing the clocks, the dim should be 0"); @@ -106,9 +106,9 @@ pub mod clock_removal_tests { fn test_no_used_clock_multi() { const PATH: &str = "samples/json/AG"; let mut dim = 0; - let mut lhs = read_json_component(PATH, "A"); + let mut lhs = read_json_automaton(PATH, "A"); lhs.set_clock_indices(&mut dim); - let mut rhs = read_json_component(PATH, "A"); + let mut rhs = read_json_automaton(PATH, "A"); rhs.set_clock_indices(&mut dim); assert_eq!( @@ -120,8 +120,8 @@ pub mod clock_removal_tests { 8 ); - let l = SystemRecipe::Component(Box::from(lhs)); - let r = SystemRecipe::Component(Box::from(rhs)); + let l = SystemRecipe::Automaton(Box::from(lhs)); + let r = SystemRecipe::Automaton(Box::from(rhs)); clock_reduction::clock_reduce(&mut Box::from(l), Some(&mut Box::from(r)), &mut dim, None) .unwrap(); assert_eq!(dim, 0, "After removing the clocks, the dim should be 0"); diff --git a/src/tests/ClockReduction/helper.rs b/src/tests/ClockReduction/helper.rs index 73f76a37..1ac32d0d 100644 --- a/src/tests/ClockReduction/helper.rs +++ b/src/tests/ClockReduction/helper.rs @@ -1,7 +1,7 @@ #[cfg(test)] pub mod test { use crate::extract_system_rep::SystemRecipe; - use crate::DataReader::json_reader::read_json_component; + use crate::DataReader::json_reader::read_json_automaton; use crate::System::input_enabler; use crate::TransitionSystems::transition_system::ClockReductionInstruction; use crate::TransitionSystems::TransitionSystemPtr; @@ -14,8 +14,8 @@ pub mod test { pub fn read_json_component_and_process( project_path: &str, component_name: &str, - ) -> component::Component { - let mut component = read_json_component(project_path, component_name); + ) -> component::Automaton { + let mut component = read_json_automaton(project_path, component_name); let inputs = component.get_input_actions(); input_enabler::make_input_enabled(&mut component, &inputs); component @@ -79,8 +79,8 @@ pub mod test { let mut component_loader = project_loader.to_comp_loader(); let mut next_clock_index: usize = 0; - let mut component1 = component_loader.get_component(comp1).clone(); - let mut component2 = component_loader.get_component(comp2).clone(); + let mut component1 = component_loader.get_automaton(comp1).clone(); + let mut component2 = component_loader.get_automaton(comp2).clone(); component1.set_clock_indices(&mut next_clock_index); component2.set_clock_indices(&mut next_clock_index); @@ -88,8 +88,8 @@ pub mod test { let dimensions = component1.declarations.clocks.len() + component2.declarations.clocks.len(); - let sr_component1 = Box::new(SystemRecipe::Component(Box::new(component1))); - let sr_component2 = Box::new(SystemRecipe::Component(Box::new(component2))); + let sr_component1 = Box::new(SystemRecipe::Automaton(Box::new(component1))); + let sr_component2 = Box::new(SystemRecipe::Automaton(Box::new(component2))); let conjunction = SystemRecipe::Conjunction(sr_component1, sr_component2); (dimensions, conjunction) @@ -106,8 +106,8 @@ pub mod test { let mut component_loader = project_loader.to_comp_loader(); let mut next_clock_index: usize = 0; - let mut component1 = component_loader.get_component(comp1).clone(); - let mut component2 = component_loader.get_component(comp2).clone(); + let mut component1 = component_loader.get_automaton(comp1).clone(); + let mut component2 = component_loader.get_automaton(comp2).clone(); component1.set_clock_indices(&mut next_clock_index); component2.set_clock_indices(&mut next_clock_index); @@ -115,8 +115,8 @@ pub mod test { let dimensions = component1.declarations.clocks.len() + component2.declarations.clocks.len(); - let sr_component1 = Box::new(SystemRecipe::Component(Box::new(component1))); - let sr_component2 = Box::new(SystemRecipe::Component(Box::new(component2))); + let sr_component1 = Box::new(SystemRecipe::Automaton(Box::new(component1))); + let sr_component2 = Box::new(SystemRecipe::Automaton(Box::new(component2))); let conjunction = SystemRecipe::Composition(sr_component1, sr_component2); diff --git a/src/tests/ClockReduction/redundant_clock_detection_test.rs b/src/tests/ClockReduction/redundant_clock_detection_test.rs index 61a7c9c5..088e61bc 100644 --- a/src/tests/ClockReduction/redundant_clock_detection_test.rs +++ b/src/tests/ClockReduction/redundant_clock_detection_test.rs @@ -3,7 +3,7 @@ pub mod test { use crate::tests::ClockReduction::helper::test::{ assert_duplicate_clock_in_clock_reduction_instruction_vec, read_json_component_and_process, }; - use crate::TransitionSystems::{CompiledComponent, TransitionSystem}; + use crate::TransitionSystems::{SimpleTransitionSystem, TransitionSystem}; use edbm::util::constraints::ClockIndex; use std::collections::HashSet; @@ -16,7 +16,7 @@ pub mod test { let component = read_json_component_and_process(REDUNDANT_CLOCKS_TEST_PROJECT, "Component1"); let compiled_component = - CompiledComponent::compile(component.clone(), DIM, &mut 0).unwrap(); + SimpleTransitionSystem::compile(component.clone(), DIM, &mut 0).unwrap(); let clock_index_x = component .declarations .get_clock_index_by_name(&expected_clocks[0]) diff --git a/src/tests/ClockReduction/unused_clock_detection_test.rs b/src/tests/ClockReduction/unused_clock_detection_test.rs index 405a966c..307abc38 100644 --- a/src/tests/ClockReduction/unused_clock_detection_test.rs +++ b/src/tests/ClockReduction/unused_clock_detection_test.rs @@ -1,18 +1,18 @@ #[cfg(test)] mod unused_clocks_tests { use crate::tests::ClockReduction::helper::test::assert_unused_clock_in_clock_reduction_instruction_vec; - use crate::DataReader::json_reader::read_json_component; - use crate::TransitionSystems::{CompiledComponent, TransitionSystem}; + use crate::DataReader::json_reader::read_json_automaton; + use crate::TransitionSystems::{SimpleTransitionSystem, TransitionSystem}; /// Loads the sample in `samples/json/ClockReductionTest/UnusedClockWithCycle` which contains /// unused clocks. It then tests that these clocks are located correctly. fn unused_clocks_with_cycles(component_name: &str, unused_clock: &str) { - let component = read_json_component( + let component = read_json_automaton( "samples/json/ClockReductionTest/UnusedClockWithCycle", component_name, ); - let compiled_component = CompiledComponent::compile( + let compiled_component = SimpleTransitionSystem::compile( component.clone(), component.declarations.clocks.len() + 1, &mut 0, @@ -32,12 +32,12 @@ mod unused_clocks_tests { /// Loads the sample in `samples/json/ClockReductionTest/UnusedClock` which contains /// unused clocks. It then tests that these clocks are located correctly. fn unused_clock(component_name: &str, unused_clock: &str) { - let component = read_json_component( + let component = read_json_automaton( "samples/json/ClockReductionTest/UnusedClock", component_name, ); - let compiled_component = CompiledComponent::compile( + let compiled_component = SimpleTransitionSystem::compile( component.clone(), component.declarations.clocks.len() + 1, &mut 0, diff --git a/src/tests/edge_ids/edge_tests.rs b/src/tests/edge_ids/edge_tests.rs index 9eb2c910..fc6d2045 100644 --- a/src/tests/edge_ids/edge_tests.rs +++ b/src/tests/edge_ids/edge_tests.rs @@ -1,13 +1,13 @@ #[cfg(test)] mod reachability_edge_test { - use crate::DataReader::json_reader::read_json_component; + use crate::DataReader::json_reader::read_json_automaton; use test_case::test_case; const FOLDER_PATH: &str = "samples/json/EcdarUniversity"; #[test_case("Machine", vec!["E25".to_string(), "E26".to_string(), "E27".to_string(), "E28".to_string(), "E29".to_string()]; "Edge ID test on Machine from the ECDAR University")] fn edge_id_checking(component_name: &str, edge_ids: Vec) { - let component = read_json_component(FOLDER_PATH, component_name); + let component = read_json_automaton(FOLDER_PATH, component_name); for (i, edge) in component.edges.iter().enumerate() { assert_eq!(edge.id, edge_ids[i]); } diff --git a/src/tests/edge_ids/saving_transitionid.rs b/src/tests/edge_ids/saving_transitionid.rs index 5c75a1ea..9d230110 100644 --- a/src/tests/edge_ids/saving_transitionid.rs +++ b/src/tests/edge_ids/saving_transitionid.rs @@ -1,6 +1,6 @@ #[cfg(test)] mod saving_transitionid_test { - use crate::System::save_component::{combine_components, PruningStrategy}; + use crate::System::save_component::{combine_automata, PruningStrategy}; use crate::{ tests::reachability::helper_functions::reachability_test_helper_functions, ModelObjects::representations::QueryExpression, @@ -42,7 +42,7 @@ mod saving_transitionid_test { FOLDER_PATH, ); - let mut comp = combine_components(&system, PruningStrategy::NoPruning); + let mut comp = combine_automata(&system, PruningStrategy::NoPruning); comp.remake_edge_ids(); diff --git a/src/tests/reachability/partial_state.rs b/src/tests/reachability/partial_state.rs index 416d2e72..8672b8c8 100644 --- a/src/tests/reachability/partial_state.rs +++ b/src/tests/reachability/partial_state.rs @@ -1,8 +1,9 @@ #[cfg(test)] mod reachability_partial_states_test { - use crate::component::{Declarations, Location}; + use crate::component::Declarations; + use crate::ModelObjects::location::{Location, LocationType}; use crate::TransitionSystems::CompositionType; - use crate::{component::LocationType, TransitionSystems::LocationTree}; + use crate::TransitionSystems::LocationTree; use test_case::test_case; fn build_location_tree_helper(id: &str, location_type: LocationType) -> LocationTree { diff --git a/src/tests/reachability/split_component_tests.rs b/src/tests/reachability/split_component_tests.rs index 8b92010e..f1c250ce 100644 --- a/src/tests/reachability/split_component_tests.rs +++ b/src/tests/reachability/split_component_tests.rs @@ -74,10 +74,7 @@ mod reachability_search_algorithm_test { ]; "Path")] fn split_component_test(path: Vec, expected: Vec>>) { - assert_eq!( - TransitionID::split_into_component_lists(&path), - Ok(expected) - ); + assert_eq!(TransitionID::split_into_automata_lists(&path), Ok(expected)); } #[test_case( @@ -100,7 +97,7 @@ mod reachability_search_algorithm_test { "Different structures 2")] fn split_component_invalid_input(path: Vec) { assert!( - TransitionID::split_into_component_lists(&path).is_err(), + TransitionID::split_into_automata_lists(&path).is_err(), "Expected error" ) } diff --git a/src/tests/refinement/Helper.rs b/src/tests/refinement/Helper.rs index 054ebbe2..01c3d87b 100644 --- a/src/tests/refinement/Helper.rs +++ b/src/tests/refinement/Helper.rs @@ -5,7 +5,7 @@ use crate::DataReader::parse_queries; use crate::ModelObjects::queries::Query; use crate::System::extract_system_rep::create_executable_query; use crate::System::query_failures::QueryResult; -use crate::TransitionSystems::transition_system::component_loader_to_transition_system; +use crate::TransitionSystems::transition_system::automata_loader_to_transition_system; use crate::TransitionSystems::TransitionSystemPtr; fn try_setup_logging() { @@ -72,5 +72,5 @@ pub fn json_get_system(PATH: &str, COMP: &str) -> TransitionSystemPtr { let project_loader = JsonProjectLoader::new_loader(String::from(PATH), crate::tests::TEST_SETTINGS); let mut loader = project_loader.to_comp_loader(); - component_loader_to_transition_system(&mut *loader, COMP) + automata_loader_to_transition_system(&mut *loader, COMP) } diff --git a/src/tests/sample.rs b/src/tests/sample.rs index 2ca358f2..22721559 100644 --- a/src/tests/sample.rs +++ b/src/tests/sample.rs @@ -10,7 +10,7 @@ mod samples { CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS, ); - let t1 = project_loader.get_component("Test1"); + let t1 = project_loader.get_automaton("Test1"); assert_eq!(t1.get_name(), "Test1"); assert_eq!(t1.get_locations().len(), 2); @@ -22,7 +22,7 @@ mod samples { CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS, ); - let t2 = project_loader.get_component("Test2"); + let t2 = project_loader.get_automaton("Test2"); assert_eq!(t2.get_name(), "Test2"); assert_eq!(t2.get_locations().len(), 2); @@ -34,7 +34,7 @@ mod samples { CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS, ); - let t3 = project_loader.get_component("Test3"); + let t3 = project_loader.get_automaton("Test3"); assert_eq!(t3.get_name(), "Test3"); assert_eq!(t3.get_locations().len(), 3); @@ -48,7 +48,7 @@ mod samples { ); for i in 1..12 { - let t = project_loader.get_component(&format!("Test{}", i).to_string()); + let t = project_loader.get_automaton(&format!("Test{}", i).to_string()); assert_eq!(t.name, format!("Test{}", i)); } diff --git a/src/tests/save_component/save_comp_helper.rs b/src/tests/save_component/save_comp_helper.rs index 75472a2e..af50e55f 100644 --- a/src/tests/save_component/save_comp_helper.rs +++ b/src/tests/save_component/save_comp_helper.rs @@ -7,7 +7,7 @@ pub mod util { use crate::System::extract_system_rep::SystemRecipe; use crate::System::query_failures::ConsistencyResult; use crate::System::refine; - use crate::System::save_component::combine_components; + use crate::System::save_component::combine_automata; use crate::System::save_component::PruningStrategy; use edbm::util::constraints::ClockIndex; @@ -47,9 +47,9 @@ pub mod util { if new_comp.is_err() { return; } - let new_comp = combine_components(&new_comp.unwrap(), PruningStrategy::NoPruning); + let new_comp = combine_automata(&new_comp.unwrap(), PruningStrategy::NoPruning); - let new_comp = SystemRecipe::Component(Box::new(new_comp)) + let new_comp = SystemRecipe::Automaton(Box::new(new_comp)) .compile(dim) .unwrap(); //TODO:: if it can fail unwrap should be replaced.