taco_cli/cli/
output_formats.rs

1//! This module contains the logic to output a GeneralThresholdAutomaton into
2//! a specific format
3
4use taco_display_utils::indent_all;
5use taco_model_checker::eltl::ELTLSpecification;
6use taco_threshold_automaton::{
7    ThresholdAutomaton, general_threshold_automaton::GeneralThresholdAutomaton,
8};
9
10/// Translate a [GeneralThresholdAutomaton] and [ELTLSpecification] into ByMC
11/// specification
12pub fn into_bymc(ta: &GeneralThresholdAutomaton, spec: &ELTLSpecification) -> String {
13    let ta_body = ta.get_ta_body_in_bymc_format();
14    let spec = spec.to_string();
15
16    let ta_full = ta_body + "\n\n" + &spec;
17
18    format!(
19        "thresholdAutomaton {} {{\n{}\n}}\n",
20        ta.name(),
21        indent_all(ta_full)
22    )
23}
24
25/// Translate a [GeneralThresholdAutomaton] and [ELTLSpecification] into TLA+
26/// specification
27///
28// TODO: implement
29pub fn into_tla(_ta: &GeneralThresholdAutomaton, _spec: &ELTLSpecification) -> String {
30    unimplemented!("TLA+ conversion has not been implemented yet :(")
31}
32
33#[cfg(test)]
34mod tests {
35    use std::{env, fs};
36
37    use taco_parser::{ParseTAWithLTL, bymc::ByMCParser, tla::TLAParser};
38    use walkdir::WalkDir;
39
40    use crate::cli::output_formats::{into_bymc, into_tla};
41
42    const EXAMPLES_FOLDER: &str = "../../examples/tla";
43
44    #[test]
45    fn test_all_examples_translate_valid() {
46        println!("Start {}", env::current_dir().unwrap().display());
47
48        for entry in WalkDir::new(EXAMPLES_FOLDER)
49            .follow_links(true)
50            .into_iter()
51            .filter_map(|e| e.ok())
52        {
53            let f_name = entry.file_name().to_string_lossy();
54            println!("Found file or folder {}", entry.path().to_string_lossy());
55
56            if f_name.ends_with(".tla") {
57                println!("Checking file {f_name}");
58
59                let spec_str = fs::read_to_string(entry.path()).unwrap();
60
61                let parser = TLAParser {};
62                let (ta, spec) = parser.parse_ta_and_spec(&spec_str).unwrap();
63
64                let new_input = into_bymc(&ta, &spec);
65
66                let bymc_parser = ByMCParser;
67                let (new_ta, new_spec) = bymc_parser.parse_ta_and_spec(&new_input).unwrap();
68
69                assert_eq!(ta, new_ta);
70                assert_eq!(spec, new_spec);
71
72                println!("Parsed TLA specification successfully");
73            }
74        }
75    }
76
77    #[test]
78    #[should_panic]
79    fn test_into_tla() {
80        println!("Start {}", env::current_dir().unwrap().display());
81
82        for entry in WalkDir::new(EXAMPLES_FOLDER)
83            .follow_links(true)
84            .into_iter()
85            .filter_map(|e| e.ok())
86        {
87            let f_name = entry.file_name().to_string_lossy();
88            println!("Found file or folder {}", entry.path().to_string_lossy());
89
90            if f_name.ends_with(".tla") {
91                println!("Checking file {f_name}");
92
93                let spec_str = fs::read_to_string(entry.path()).unwrap();
94
95                let parser = ByMCParser {};
96                let (ta, spec) = parser.parse_ta_and_spec(&spec_str).unwrap();
97
98                let new_input = into_tla(&ta, &spec);
99
100                let bymc_parser = TLAParser {};
101                let (new_ta, new_spec) = bymc_parser.parse_ta_and_spec(&new_input).unwrap();
102
103                assert_eq!(ta, new_ta);
104                assert_eq!(spec, new_spec);
105
106                println!("Parsed TLA specification successfully");
107            }
108        }
109    }
110}
taco_cli/cli/output_formats.rs

taco_cli/cli/
output_formats.rs
