modelator/artifact/
tla_file.rs

1use super::{Artifact, ArtifactCreator, ArtifactSaver};
2use crate::{Error, ModelatorRuntime};
3use core::result::Result::Err;
4use std::fs;
5use std::path::{Path, PathBuf};
6
7/// `modelator`'s artifact representing a TLA+ file.
8#[derive(Debug, Clone, PartialEq, Eq)]
9pub struct TlaFile {
10    /// TODO: file_contents backing strings are to be removed
11    file_contents_backing: String,
12    /// Module name
13    module_name: String,
14}
15
16impl TlaFile {
17    /// Returns the module name of the TLA file
18    pub fn module_name(&self) -> &str {
19        &self.module_name
20    }
21
22    /// Returns a base filename `{module_name}.tla`
23    pub fn file_name(&self) -> String {
24        format!("{}.tla", &self.module_name)
25    }
26
27    /// Returns raw file contents (string value that it was initialized with)
28    /// NOTE: will change as our internal representation of relevant TLA+ related files improves
29    pub fn file_contents_backing(&self) -> &str {
30        &self.file_contents_backing
31    }
32}
33
34impl ArtifactCreator for TlaFile {
35    /// Create a new instance from a file content string.
36    fn from_string(s: &str) -> Result<Self, Error> {
37        match module_name(s) {
38            Err(_) => Err(Error::MissingTlaFileModuleName(s.to_string())),
39            Ok(name) => Ok(Self {
40                file_contents_backing: s.to_string(),
41                module_name: name,
42            }),
43        }
44    }
45}
46
47impl Artifact for TlaFile {
48    fn as_string(&self) -> String {
49        // TODO: will use explicit data to generate a repr
50        self.file_contents_backing.clone()
51    }
52}
53
54impl ArtifactSaver for TlaFile {
55    fn filename(&self) -> String {
56        format!("{}.tla", self.module_name())
57    }
58}
59
60impl std::fmt::Display for TlaFile {
61    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
62        write!(f, "{}", &self.file_contents_backing)
63    }
64}
65
66#[derive(Debug, PartialEq, Eq)]
67struct ModuleNameParseError;
68
69fn module_name(file_content: &str) -> Result<String, ModuleNameParseError> {
70    let substr = "MODULE";
71    for line in file_content.split('\n') {
72        if line.contains(substr) {
73            let segments = line.split_whitespace().collect::<Vec<&str>>();
74            if segments.len() != 4 {
75                return Err(ModuleNameParseError);
76            }
77            return Ok(segments[2].to_string());
78        } else if !line.trim().is_empty() {
79            // Line not whitespace but also does not contain module name
80            // -> invalid TLA file.
81            return Err(ModuleNameParseError);
82        }
83    }
84    Err(ModuleNameParseError)
85}
86
87#[cfg(test)]
88mod tests {
89    use super::*;
90
91    #[test]
92    fn test_module_parse() {
93        let s = "\n---------- MODULE moduleName ----------\n42";
94        assert_eq!(module_name(s), Ok("moduleName".into()));
95    }
96}
modelator/artifact/tla_file.rs

modelator/artifact/
tla_file.rs
