From 512c36ef45c40166b047b6d767f92e47cd50ed7b Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Thu, 30 Mar 2023 18:05:47 +0200 Subject: [PATCH 1/6] Update list of authors in Cargo.toml --- Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index 9ca41880..eb409e8e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,7 +2,7 @@ name = "reveaal" version = "0.1.0" build = "src/build.rs" -authors = ["Peter Greve "] +authors = ["Thomas Lohse", "Sebastian Lund", "Thorulf Neustrup", "Peter Greve"] edition = "2018" [lib] From 705e28848830f095187044e56987c5650438286e Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Thu, 30 Mar 2023 18:07:56 +0200 Subject: [PATCH 2/6] Switch from clap yaml to clap derive, and use PathBufs instead of &str for paths (its safer) --- Cargo.toml | 4 +- benches/clock_reduction_bench.rs | 6 +- src/DataReader/component_loader.rs | 19 ++--- src/DataReader/json_reader.rs | 52 +++++++------ src/DataReader/json_writer.rs | 15 ++-- src/DataReader/xml_parser.rs | 9 ++- src/cli.rs | 59 +++++++++++++++ src/cli.yml | 50 ------------- src/lib.rs | 1 + src/main.rs | 86 ++++++++++++---------- src/tests/ClockReduction/helper.rs | 3 +- src/tests/reachability/helper_functions.rs | 4 +- src/tests/sample.rs | 8 +- 13 files changed, 169 insertions(+), 147 deletions(-) create mode 100644 src/cli.rs delete mode 100644 src/cli.yml diff --git a/Cargo.toml b/Cargo.toml index eb409e8e..9715814b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,14 +20,14 @@ logging = ["dep:env_logger", "dep:chrono"] [dependencies] serde_json = "1.0" serde = { version = "1.0", features = ["derive"] } -clap = { version = "~2.34.0", features = ["yaml"] } +clap = { version = "4.2.1", features = [ "derive" ] } pest = "2.1.3" pest_derive = "2.1.0" xml-rs = "0.8.3" serde-xml-rs = "0.6.0" elementtree = "1.2.2" dyn-clone = "1.0" -tonic = "0.8.2" +tonic = "0.8.3" prost = "0.11.0" tokio = { version = "1.0", features = ["macros", "rt"] } colored = "2.0.0" diff --git a/benches/clock_reduction_bench.rs b/benches/clock_reduction_bench.rs index cbcad63f..9b03ef1f 100644 --- a/benches/clock_reduction_bench.rs +++ b/benches/clock_reduction_bench.rs @@ -22,8 +22,7 @@ fn bench_clock_reduced_refinement(c: &mut Criterion) { fn clock_reduced_refinement() { let query = parse_to_query(QUERY); let mut loader = - JsonProjectLoader::new("samples/json/EcdarUniversity".to_string(), DEFAULT_SETTINGS) - .to_comp_loader(); + JsonProjectLoader::new("samples/json/EcdarUniversity", DEFAULT_SETTINGS).to_comp_loader(); let executor = create_executable_query(query.get(0).unwrap(), &mut *loader).unwrap(); executor.execute(); } @@ -31,8 +30,7 @@ fn clock_reduced_refinement() { fn normal_refinement() { let query = parse_to_query(QUERY); let mut loader = - JsonProjectLoader::new("samples/json/EcdarUniversity".to_string(), TEST_SETTINGS) - .to_comp_loader(); + JsonProjectLoader::new("samples/json/EcdarUniversity", TEST_SETTINGS).to_comp_loader(); let executor = create_executable_query(query.get(0).unwrap(), &mut *loader).unwrap(); executor.execute(); } diff --git a/src/DataReader/component_loader.rs b/src/DataReader/component_loader.rs index 696a2f2a..f443f59d 100644 --- a/src/DataReader/component_loader.rs +++ b/src/DataReader/component_loader.rs @@ -12,6 +12,7 @@ use crate::ProtobufServer::services::query_request::Settings; use crate::System::input_enabler; use std::collections::HashMap; use std::num::NonZeroUsize; +use std::path::{Path, PathBuf}; use std::sync::{Arc, Mutex}; use super::proto_reader::components_info_to_components; @@ -194,12 +195,12 @@ fn parse_xml_components(xml: &str) -> Vec { pub trait ProjectLoader: ComponentLoader { fn get_declarations(&self) -> &SystemDeclarations; fn get_queries(&self) -> &Vec; - fn get_project_path(&self) -> &str; + fn get_project_path(&self) -> &PathBuf; fn to_comp_loader(self: Box) -> Box; } pub struct JsonProjectLoader { - project_path: String, + project_path: PathBuf, loaded_components: ComponentsMap, system_declarations: SystemDeclarations, queries: Vec, @@ -240,7 +241,7 @@ impl ProjectLoader for JsonProjectLoader { &self.queries } - fn get_project_path(&self) -> &str { + fn get_project_path(&self) -> &PathBuf { &self.project_path } @@ -251,12 +252,12 @@ impl ProjectLoader for JsonProjectLoader { impl JsonProjectLoader { #[allow(clippy::new_ret_no_self)] - pub fn new(project_path: String, settings: Settings) -> Box { + pub fn new>(project_path: P, settings: Settings) -> Box { let system_declarations = json_reader::read_system_declarations(&project_path).unwrap(); let queries = json_reader::read_queries(&project_path).unwrap(); Box::new(JsonProjectLoader { - project_path, + project_path: project_path.as_ref().to_path_buf(), loaded_components: HashMap::new(), system_declarations, queries, @@ -284,7 +285,7 @@ impl JsonProjectLoader { } pub struct XmlProjectLoader { - project_path: String, + project_path: PathBuf, loaded_components: ComponentsMap, system_declarations: SystemDeclarations, queries: Vec, @@ -319,7 +320,7 @@ impl ProjectLoader for XmlProjectLoader { &self.queries } - fn get_project_path(&self) -> &str { + fn get_project_path(&self) -> &PathBuf { &self.project_path } @@ -330,7 +331,7 @@ impl ProjectLoader for XmlProjectLoader { impl XmlProjectLoader { #[allow(clippy::new_ret_no_self)] - pub fn new(project_path: String, settings: Settings) -> Box { + pub fn new>(project_path: P, settings: Settings) -> Box { let (comps, system_declarations, queries) = parse_xml_from_file(&project_path); let mut map = HashMap::::new(); @@ -345,7 +346,7 @@ impl XmlProjectLoader { } Box::new(XmlProjectLoader { - project_path, + project_path: project_path.as_ref().to_path_buf(), loaded_components: map, system_declarations, queries, diff --git a/src/DataReader/json_reader.rs b/src/DataReader/json_reader.rs index e8fe087f..7467363a 100644 --- a/src/DataReader/json_reader.rs +++ b/src/DataReader/json_reader.rs @@ -6,39 +6,38 @@ use std::fs::File; use std::io::Read; use std::path::Path; -pub fn read_system_declarations(project_path: &str) -> Option { - let sysdecl_path = format!( - "{}{}SystemDeclarations.json", - project_path, - std::path::MAIN_SEPARATOR - ); +pub fn read_system_declarations>(project_path: P) -> Option { + let sysdecl_path = project_path.as_ref().join("SystemDeclarations.json"); if !Path::new(&sysdecl_path).exists() { return None; } - match read_json::(&sysdecl_path) { + match read_json::(&sysdecl_path) { Ok(sys_decls) => Some(sys_decls), Err(error) => panic!( "We got error {}, and could not parse json file {} to component", - error, &sysdecl_path + error, + sysdecl_path.display() ), } } -pub fn read_json_component(project_path: &str, component_name: &str) -> component::Component { - let component_path = format!( - "{0}{1}Components{1}{2}.json", - project_path, - std::path::MAIN_SEPARATOR, - component_name - ); +pub fn read_json_component>( + project_path: P, + component_name: &str, +) -> component::Component { + let component_path = project_path + .as_ref() + .join("Components") + .join(format!("{}.json", component_name)); let component: component::Component = match read_json(&component_path) { Ok(json) => json, Err(error) => panic!( "We got error {}, and could not parse json file {} to component", - error, component_path + error, + component_path.display() ), }; @@ -48,14 +47,18 @@ pub fn read_json_component(project_path: &str, component_name: &str) -> componen //Input:File name //Description:uses the filename to open the file and then reads the file. //Output: Result type, if more info about this type is need please go to: https://doc.rust-lang.org/std/result/ -pub fn read_json(filename: &str) -> serde_json::Result { - let mut file = - File::open(filename).unwrap_or_else(|_| panic!("Could not find file {}", filename)); +pub fn read_json>(filename: P) -> serde_json::Result { + let mut file = File::open(&filename) + .unwrap_or_else(|_| panic!("Could not find file {}", filename.as_ref().display())); let mut data = String::new(); file.read_to_string(&mut data).unwrap(); - let json_file = serde_json::from_str(&data) - .unwrap_or_else(|_| panic!("{}: Json format is not as expected", filename)); + let json_file = serde_json::from_str(&data).unwrap_or_else(|_| { + panic!( + "{}: Json format is not as expected", + filename.as_ref().display() + ) + }); Ok(json_file) } @@ -67,8 +70,8 @@ pub fn json_to_component(json_str: &str) -> Result Option> { - let queries_path = format!("{}{}Queries.json", project_path, std::path::MAIN_SEPARATOR); +pub fn read_queries>(project_path: P) -> Option> { + let queries_path = project_path.as_ref().join("Queries.json"); if !Path::new(&queries_path).exists() { return None; @@ -78,7 +81,8 @@ pub fn read_queries(project_path: &str) -> Option> { Ok(json) => Some(json), Err(error) => panic!( "We got error {}, and could not parse json file {} to query", - error, &queries_path + error, + queries_path.display() ), } } diff --git a/src/DataReader/json_writer.rs b/src/DataReader/json_writer.rs index b5c4c83e..1a70d81b 100644 --- a/src/DataReader/json_writer.rs +++ b/src/DataReader/json_writer.rs @@ -1,13 +1,12 @@ use crate::ModelObjects::component::Component; -use std::fs::File; +use std::{fs::File, path::Path}; + +pub fn component_to_json_file>(project_path: P, component: &Component) { + let path = project_path + .as_ref() + .join("Components") + .join(format!("{}.json", component.get_name())); -pub fn component_to_json_file(project_path: &str, component: &Component) { - let path = format!( - "{0}{1}Components{1}{2}.json", - project_path, - std::path::MAIN_SEPARATOR, - component.get_name() - ); let file = File::create(path).expect("Couldnt open file"); serde_json::to_writer_pretty(&file, component).expect("Failed to serialize component"); diff --git a/src/DataReader/xml_parser.rs b/src/DataReader/xml_parser.rs index 54fbbbb4..6ee3d84a 100644 --- a/src/DataReader/xml_parser.rs +++ b/src/DataReader/xml_parser.rs @@ -9,14 +9,15 @@ use std::collections::HashMap; use std::fs::File; use std::io::BufReader; use std::io::Read; +use std::path::Path; -pub fn is_xml_project(project_path: &str) -> bool { - project_path.ends_with(".xml") +pub fn is_xml_project>(project_path: P) -> bool { + project_path.as_ref().ends_with(".xml") } ///Used to parse systems described in xml -pub(crate) fn parse_xml_from_file( - fileName: &str, +pub(crate) fn parse_xml_from_file>( + fileName: P, ) -> ( Vec, system_declarations::SystemDeclarations, diff --git a/src/cli.rs b/src/cli.rs new file mode 100644 index 00000000..83611f20 --- /dev/null +++ b/src/cli.rs @@ -0,0 +1,59 @@ +use clap::Parser; +use std::path::PathBuf; + +#[derive(Parser)] +#[command(author, version, + about="Reveaal is a model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems)\nFor more information about ECDAR see https://www.ecdar.net/", + long_about = Some("With Reveaal you can either run a single query with the 'query' command or run it as a server with the 'serve' command"))] +pub enum Args { + /// Start a gRPC server with the protocol defined in the protobuf file + /// + /// Examples of usage: + /// + /// Reveaal serve 127.0.0.1:4242 + /// + /// Reveaal serve -t 1 -c 50 127.0.0.1:4242 + Serve { + /// Ip address and port to serve the gRPC server on + #[clap(value_name = "IP:PORT")] + endpoint: String, + + /// The number of threads to use when running queries on the server + #[arg(short, long, default_value_t = num_cpus::get())] + thread_count: usize, + + /// The maximal number of component saved in the server cache + #[arg(short, long, default_value_t = 100)] + cache_size: usize, + }, + /// Run a query + /// + /// Examples of usage: + /// + /// Reveaal query "refinement: Researcher || Machine || Administration <= Spec" -i samples/json/EcdarUniversity + /// + /// Reveaal query "consistency: Machine" -i samples/json/EcdarUniversity + /// + /// Reveaal query "determinism: Researcher" -i samples/json/EcdarUniversity + Query { + /// The query to execute + #[clap(value_name = "QUERY_TYPE: QUERY")] + query: String, + + /// File (XML) or folder (JSON) with component definitions + #[arg(short, long, value_name = "XML|JSON")] + input_folder: PathBuf, + + /// Whether to disable clock reduction + #[arg(short, long, default_value_t = false)] + disable_clock_reduction: bool, + + /// Save file for refinement relations + #[arg(short, long, value_name = "FILE")] + save_refinement_relations: Option, + // TODO: Maybe add this later + // /// The number of threads to use when running the query + // #[arg(short, long, default_value_t = num_cpus::get())] + // thread_count: usize, + }, +} \ No newline at end of file diff --git a/src/cli.yml b/src/cli.yml deleted file mode 100644 index dfaa7f6a..00000000 --- a/src/cli.yml +++ /dev/null @@ -1,50 +0,0 @@ -name: reveaal -version: "1.0" -about: Rust engine for ecdar -args: - - endpoint: - short: p - long: proto - required: false - takes_value: true - - folder: - short: i - long: input-folder - #help: input folder with components as json and a Queries.json file - required: false - takes_value: true - default_value: "." - #index: 1 - - query: - #short: q - #long: query - #help: query in a format of function:component<=component, if -query is present, the queries file will be ignored - required: false - takes_value: true - index: 1 - - save-relation: - short: s - long: save-relation - required: false - takes_value: false - - clock-reduction: - long: disable-clock-reduction - required: false - takes_value: false - - cache-size: - short: cs - long: cache-size - required: false - takes_value: true - default_value: "100" - - thread-number: - short: tn - long: thread-number - required: false - takes_value: true -# - checkInputOutput: -# short: c -# long: checkInputOutput -# help: returns extra ouputs which are present on the left side and vise versa inputs -# required: false -# takes_value: false diff --git a/src/lib.rs b/src/lib.rs index e8a6c57c..6e95c27d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -7,6 +7,7 @@ pub mod ProtobufServer; pub mod Simulation; pub mod System; pub mod TransitionSystems; +pub mod cli; pub mod logging; pub mod tests; diff --git a/src/main.rs b/src/main.rs index db2a2ab0..a69f6815 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,43 +1,37 @@ #![allow(non_snake_case)] -use clap::{load_yaml, App}; +use reveaal::cli::Args; use reveaal::logging::setup_logger; use reveaal::System::query_failures::QueryResult; +use clap::Parser; use reveaal::ProtobufServer::services::query_request::Settings; use reveaal::{ extract_system_rep, parse_queries, start_grpc_server_with_tokio, xml_parser, ComponentLoader, JsonProjectLoader, ProjectLoader, Query, XmlProjectLoader, }; use std::env; +use std::path::Path; fn main() -> Result<(), Box> { + let args = Args::parse(); + #[cfg(feature = "logging")] - let yaml = load_yaml!("cli.yml"); - let matches = App::from(yaml).get_matches(); setup_logger().unwrap(); - if let Some(ip_endpoint) = matches.value_of("endpoint") { - let thread_count: usize = match matches.value_of("thread_number") { - Some(num_of_threads) => num_of_threads - .parse() - .expect("Could not parse the input for the number of threads"), - None => num_cpus::get(), - }; - let cache_count: usize = matches - .value_of("cache-size") - .unwrap() - .parse() - .expect("Could not parse input for the cache_size"); - - start_grpc_server_with_tokio(ip_endpoint, cache_count, thread_count)?; - } else { - start_using_cli(&matches); + + match args { + Args::Serve { + endpoint, + thread_count, + cache_size, + } => start_grpc_server_with_tokio(&endpoint, cache_size, thread_count)?, + Args::Query { .. } => start_using_cli(args), } Ok(()) } -fn start_using_cli(matches: &clap::ArgMatches) { - let (mut comp_loader, queries) = parse_args(matches); +fn start_using_cli(args: Args) { + let (mut comp_loader, queries) = parse_args(args); let mut results = vec![]; for query in &queries { @@ -60,25 +54,41 @@ fn start_using_cli(matches: &clap::ArgMatches) { } } -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 { - disable_clock_reduction: matches.is_present("clock-reduction"), - }; - - let project_loader = get_project_loader(folder_path.to_string(), settings); - - let queries = if query.is_empty() { - project_loader.get_queries().clone() - } else { - parse_queries::parse_to_query(query) - }; - - (project_loader.to_comp_loader(), queries) +fn parse_args(args: Args) -> (Box, Vec) { + match args { + Args::Query { + query, + input_folder, + disable_clock_reduction, + save_refinement_relations, + //thread_count, + } => { + if save_refinement_relations.is_some() { + unimplemented!("Saving refinement relations is not yet implemented"); + } + + let settings = Settings { + disable_clock_reduction, + }; + + let project_loader = get_project_loader(input_folder, settings); + + let queries = if query.is_empty() { + project_loader.get_queries().clone() + } else { + parse_queries::parse_to_query(&query) + }; + + (project_loader.to_comp_loader(), queries) + } + _ => unreachable!("This function should only be called when the args are a query"), + } } -fn get_project_loader(project_path: String, settings: Settings) -> Box { +fn get_project_loader>( + project_path: P, + settings: Settings, +) -> Box { if xml_parser::is_xml_project(&project_path) { XmlProjectLoader::new(project_path, settings) } else { diff --git a/src/tests/ClockReduction/helper.rs b/src/tests/ClockReduction/helper.rs index 6caeae80..ae539e8d 100644 --- a/src/tests/ClockReduction/helper.rs +++ b/src/tests/ClockReduction/helper.rs @@ -100,8 +100,7 @@ pub mod test { comp1: &str, comp2: &str, ) -> TransitionSystemPtr { - let project_loader = - JsonProjectLoader::new(path.to_string_lossy().to_string(), DEFAULT_SETTINGS); + let project_loader = JsonProjectLoader::new(path, DEFAULT_SETTINGS); let mut component_loader = project_loader.to_comp_loader(); diff --git a/src/tests/reachability/helper_functions.rs b/src/tests/reachability/helper_functions.rs index b2998906..1c9f17f7 100644 --- a/src/tests/reachability/helper_functions.rs +++ b/src/tests/reachability/helper_functions.rs @@ -60,9 +60,9 @@ pub mod reachability_test_helper_functions { folder_path: &str, ) -> (Box, Box) { let mut comp_loader = if xml_parser::is_xml_project(folder_path) { - XmlProjectLoader::new(folder_path.to_string(), crate::tests::TEST_SETTINGS) + XmlProjectLoader::new(folder_path, crate::tests::TEST_SETTINGS) } else { - JsonProjectLoader::new(folder_path.to_string(), crate::tests::TEST_SETTINGS) + JsonProjectLoader::new(folder_path, crate::tests::TEST_SETTINGS) } .to_comp_loader(); let mut dim: ClockIndex = 0; diff --git a/src/tests/sample.rs b/src/tests/sample.rs index 8000fd15..5cd6f96f 100644 --- a/src/tests/sample.rs +++ b/src/tests/sample.rs @@ -7,7 +7,7 @@ mod samples { #[test] fn test_locations_T1() { let mut project_loader = - JsonProjectLoader::new(CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS); + JsonProjectLoader::new(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); let t1 = project_loader.get_component("Test1"); assert_eq!(t1.get_name(), "Test1"); @@ -17,7 +17,7 @@ mod samples { #[test] fn test_locations_T2() { let mut project_loader = - JsonProjectLoader::new(CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS); + JsonProjectLoader::new(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); let t2 = project_loader.get_component("Test2"); assert_eq!(t2.get_name(), "Test2"); @@ -27,7 +27,7 @@ mod samples { #[test] fn test_locations_T3() { let mut project_loader = - JsonProjectLoader::new(CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS); + JsonProjectLoader::new(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); let t3 = project_loader.get_component("Test3"); assert_eq!(t3.get_name(), "Test3"); @@ -37,7 +37,7 @@ mod samples { #[test] fn test_names_T1_through_T12() { let mut project_loader = - JsonProjectLoader::new(CONJUNCTION_SAMPLE.to_string(), crate::tests::TEST_SETTINGS); + JsonProjectLoader::new(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); for i in 1..12 { let t = project_loader.get_component(&format!("Test{}", i).to_string()); From 9a1ad09064e8f0f955f0d91e753caadf9b38b070 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Thu, 30 Mar 2023 18:33:34 +0200 Subject: [PATCH 3/6] Cargo fmt --- src/cli.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/cli.rs b/src/cli.rs index 83611f20..7feb4eb8 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -7,11 +7,11 @@ use std::path::PathBuf; long_about = Some("With Reveaal you can either run a single query with the 'query' command or run it as a server with the 'serve' command"))] pub enum Args { /// Start a gRPC server with the protocol defined in the protobuf file - /// + /// /// Examples of usage: - /// + /// /// Reveaal serve 127.0.0.1:4242 - /// + /// /// Reveaal serve -t 1 -c 50 127.0.0.1:4242 Serve { /// Ip address and port to serve the gRPC server on @@ -27,13 +27,13 @@ pub enum Args { cache_size: usize, }, /// Run a query - /// + /// /// Examples of usage: - /// + /// /// Reveaal query "refinement: Researcher || Machine || Administration <= Spec" -i samples/json/EcdarUniversity - /// + /// /// Reveaal query "consistency: Machine" -i samples/json/EcdarUniversity - /// + /// /// Reveaal query "determinism: Researcher" -i samples/json/EcdarUniversity Query { /// The query to execute @@ -56,4 +56,4 @@ pub enum Args { // #[arg(short, long, default_value_t = num_cpus::get())] // thread_count: usize, }, -} \ No newline at end of file +} From f27882068856038075680872d5045743162d4701 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Thu, 30 Mar 2023 18:36:11 +0200 Subject: [PATCH 4/6] Cargo fmt --- src/cli.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/cli.rs b/src/cli.rs index 7feb4eb8..6659d9df 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -2,9 +2,7 @@ use clap::Parser; use std::path::PathBuf; #[derive(Parser)] -#[command(author, version, - about="Reveaal is a model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems)\nFor more information about ECDAR see https://www.ecdar.net/", - long_about = Some("With Reveaal you can either run a single query with the 'query' command or run it as a server with the 'serve' command"))] +#[command(author, version, about="Reveaal is a model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems)\nFor more information about ECDAR see https://www.ecdar.net/", long_about = Some("With Reveaal you can either run a single query with the 'query' command or run it as a server with the 'serve' command"))] pub enum Args { /// Start a gRPC server with the protocol defined in the protobuf file /// From 53c556ff866f2a1ce370fcf1df158baa4353a12e Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Tue, 22 Aug 2023 21:23:56 +0200 Subject: [PATCH 5/6] Removed unnecessary func-call --- src/tests/reachability/helper_functions.rs | 4 ++-- src/tests/sample.rs | 24 ++++++++-------------- 2 files changed, 10 insertions(+), 18 deletions(-) diff --git a/src/tests/reachability/helper_functions.rs b/src/tests/reachability/helper_functions.rs index 1e7c143d..c0aa0f22 100644 --- a/src/tests/reachability/helper_functions.rs +++ b/src/tests/reachability/helper_functions.rs @@ -22,9 +22,9 @@ pub mod reachability_test_helper_functions { folder_path: &str, ) -> (Box, Box) { let mut comp_loader = if xml_parser::is_xml_project(folder_path) { - XmlProjectLoader::new_loader(folder_path.to_string(), crate::tests::TEST_SETTINGS) + XmlProjectLoader::new_loader(folder_path, crate::tests::TEST_SETTINGS) } else { - JsonProjectLoader::new_loader(folder_path.to_string(), crate::tests::TEST_SETTINGS) + JsonProjectLoader::new_loader(folder_path, crate::tests::TEST_SETTINGS) } .to_comp_loader(); let mut dim: ClockIndex = 0; diff --git a/src/tests/sample.rs b/src/tests/sample.rs index 060e7716..f6614de3 100644 --- a/src/tests/sample.rs +++ b/src/tests/sample.rs @@ -6,10 +6,8 @@ mod samples { #[test] fn test_locations_T1() { - let mut project_loader = JsonProjectLoader::new_loader( - CONJUNCTION_SAMPLE.to_string(), - crate::tests::TEST_SETTINGS, - ); + let mut project_loader = + JsonProjectLoader::new_loader(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); let t1 = project_loader.get_component("Test1"); assert_eq!(t1.name, "Test1"); @@ -18,10 +16,8 @@ mod samples { #[test] fn test_locations_T2() { - let mut project_loader = JsonProjectLoader::new_loader( - CONJUNCTION_SAMPLE.to_string(), - crate::tests::TEST_SETTINGS, - ); + let mut project_loader = + JsonProjectLoader::new_loader(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); let t2 = project_loader.get_component("Test2"); assert_eq!(t2.name, "Test2"); @@ -30,10 +26,8 @@ mod samples { #[test] fn test_locations_T3() { - let mut project_loader = JsonProjectLoader::new_loader( - CONJUNCTION_SAMPLE.to_string(), - crate::tests::TEST_SETTINGS, - ); + let mut project_loader = + JsonProjectLoader::new_loader(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); let t3 = project_loader.get_component("Test3"); assert_eq!(t3.name, "Test3"); @@ -42,10 +36,8 @@ mod samples { #[test] fn test_names_T1_through_T12() { - let mut project_loader = JsonProjectLoader::new_loader( - CONJUNCTION_SAMPLE.to_string(), - crate::tests::TEST_SETTINGS, - ); + let mut project_loader = + JsonProjectLoader::new_loader(CONJUNCTION_SAMPLE, crate::tests::TEST_SETTINGS); for i in 1..12 { let t = project_loader.get_component(&format!("Test{}", i).to_string()); From 06e8ea2e87d369e8fc8409ea06a726b0caf795cf Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Wed, 23 Aug 2023 16:13:20 +0200 Subject: [PATCH 6/6] Added tests and did some formatting --- src/DataReader/parse_queries.rs | 4 +- src/cli.rs | 114 ++++++++++++++++++++++++++++++-- src/main.rs | 4 +- 3 files changed, 114 insertions(+), 8 deletions(-) diff --git a/src/DataReader/parse_queries.rs b/src/DataReader/parse_queries.rs index 47064872..1a1f8891 100644 --- a/src/DataReader/parse_queries.rs +++ b/src/DataReader/parse_queries.rs @@ -220,8 +220,8 @@ pub fn test_parse() { } pub fn parse_to_query(input: &str) -> Vec { - let queries = parse_to_expression_tree(input).unwrap(); - queries + parse_to_expression_tree(input) + .expect("Parsing failed") .into_iter() .map(|q| Query { query: Option::from(q), diff --git a/src/cli.rs b/src/cli.rs index 6659d9df..45ad90a1 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -1,7 +1,7 @@ use clap::Parser; use std::path::PathBuf; -#[derive(Parser)] +#[derive(Parser, Debug)] #[command(author, version, about="Reveaal is a model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems)\nFor more information about ECDAR see https://www.ecdar.net/", long_about = Some("With Reveaal you can either run a single query with the 'query' command or run it as a server with the 'serve' command"))] pub enum Args { /// Start a gRPC server with the protocol defined in the protobuf file @@ -35,16 +35,16 @@ pub enum Args { /// Reveaal query "determinism: Researcher" -i samples/json/EcdarUniversity Query { /// The query to execute - #[clap(value_name = "QUERY_TYPE: QUERY")] + #[clap(value_name = "QUERY_TYPE: refinement|consistency|reachability|save-component", value_parser = query_check)] query: String, /// File (XML) or folder (JSON) with component definitions #[arg(short, long, value_name = "XML|JSON")] input_folder: PathBuf, - /// Whether to disable clock reduction + /// Whether to enable clock reduction #[arg(short, long, default_value_t = false)] - disable_clock_reduction: bool, + enable_clock_reduction: bool, /// Save file for refinement relations #[arg(short, long, value_name = "FILE")] @@ -55,3 +55,109 @@ pub enum Args { // thread_count: usize, }, } + +fn query_check(arg: &str) -> Result { + crate::parse_queries::parse_to_expression_tree(arg).map(|_| arg.to_string()) +} + +#[cfg(test)] +mod tests { + use super::Args; + use clap::Parser; + use std::path::PathBuf; + use std::str::FromStr; + use test_case::test_case; + + #[test] + fn serve_command_with_t_and_c_flags() { + println!("{:?}", PathBuf::from_str(" fucking pis path")); + // 0th argument does not matter, but it must be present + let input_args = vec!["", "serve", "-t", "10", "-c", "100", "127.0.0.1:4242"]; + let args_matches = Args::parse_from(input_args); + check_args( + args_matches, + Args::Serve { + endpoint: "127.0.0.1:4242".to_string(), + thread_count: 10, + cache_size: 100, + }, + ); + } + + #[test_case( + &["", "query", "-i", "/path/to/system", "-e", "-s", "saved-comp", "refinement: some <= refinement"], Args::Query { + query: "refinement: some <= refinement".to_string(), + input_folder: PathBuf::from("/path/to/system"), + enable_clock_reduction: true, + save_refinement_relations: Some(PathBuf::from("saved-comp")), + } ; "All fields" + )] + #[test_case( + &["", "query", "-i", "/path/to/system", "-s", "saved-comp", "refinement: some <= refinement"], Args::Query { + query: "refinement: some <= refinement".to_string(), + input_folder: PathBuf::from("/path/to/system"), + enable_clock_reduction: Default::default(), + save_refinement_relations: Some(PathBuf::from("saved-comp")), + } ; "Default clock-reduction" + )] + #[test_case( + &["", "query", "-i", "/path/to/system", "refinement: some <= refinement"], Args::Query { + query: "refinement: some <= refinement".to_string(), + input_folder: PathBuf::from("/path/to/system"), + enable_clock_reduction: Default::default(), + save_refinement_relations: None, + } ; "No saved path" + )] + fn query_command_tests(input_args: &[&str], expected: Args) { + check_args(Args::parse_from(input_args), expected); + } + + #[test_case(&["", "query", "-i", "/path/to/system", "-s", "refinement: some <= refinement"] ; "Not supplying needed argument")] + #[test_case(&["", "query", "-i", "/path/to/system", "refinement: some refinement"] ; "Bad query")] + #[test_case(&["", "serve", "-i", "/path/to/system", "refinement: some <= refinement"] ; "Wrong command")] + #[should_panic] + fn query_command_tests_panics(input_args: &[&str]) { + Args::try_parse_from(input_args).unwrap(); + } + + fn check_args(actual: Args, expected: Args) { + match (actual, expected) { + ( + Args::Query { + query: qa, + input_folder: ia, + enable_clock_reduction: da, + save_refinement_relations: sa, + }, + Args::Query { + query: qe, + input_folder: ie, + enable_clock_reduction: de, + save_refinement_relations: se, + }, + ) => { + assert_eq!(qa, qe); + assert_eq!(ia, ie); + assert_eq!(da, de); + assert_eq!(sa, se); + } + ( + Args::Serve { + endpoint: ea, + thread_count: ta, + cache_size: ca, + }, + Args::Serve { + endpoint: ee, + thread_count: te, + cache_size: ce, + }, + ) => { + assert_eq!(ea, ee); + assert_eq!(ta, te); + assert_eq!(ca, ce); + } + (a, e) => panic!("Not same, expected {:?}, got {:?}", e, a), + } + } +} diff --git a/src/main.rs b/src/main.rs index 142400c3..9d062dfe 100644 --- a/src/main.rs +++ b/src/main.rs @@ -60,7 +60,7 @@ fn parse_args(args: Args) -> (Box, Vec) { Args::Query { query, input_folder, - disable_clock_reduction, + enable_clock_reduction, save_refinement_relations, //thread_count, } => { @@ -69,7 +69,7 @@ fn parse_args(args: Args) -> (Box, Vec) { } let settings = Settings { - disable_clock_reduction, + disable_clock_reduction: !enable_clock_reduction, }; let project_loader = get_project_loader(input_folder, settings);