Expand description
List of artifacts.
Structs
modelator’s artifact containing a test trace encoded as JSON.
Ultra-basic wrapper around stdout of model checker execution NOTE: This is a stand in and will be changed soon.
modelator’s artifact representing a TLA+ config file containing the TLA+
model CONSTANTs and INIT and NEXT predicates.
modelator’s artifact representing a TLA+ file.
TODO: split module and cfg into two parts and contain the main module and extended modules in module struct An in-memory representation of all the resources needed to perform model checking Includes the main .tla and .cfg files as well as depended on (via EXTENDS) .tla files.
modelator’s artifact containing a test trace encoded as TLA+.
Traits
A wrapper around a file NOTE: for now this is bare-bones but it will eventually include additional meta-data which will justify the additional interface.
A sister trait for Artifacts for static constructor methods NOTE: static methods and polymorphic methods prevent trait-object instantiation so this approach allows dynamic use of Artifacts
An artifact which is a file It can be saved in a directory, as it has its own filename
Functions
Try to write each artifact in any object implementing into_iter for Artifacts to the given directory