Saving and loading state spaces

The Model Checker application has utilities for saving and loading state spaces. For larger systems this feature is too slow to be very practical. State spaces are stored in text files that have the extension '.ssp'.

Once a state space has been obtained either by generating it or loading it from a file you can save it by selecting the option Save State Space from the State Space menu. A file navigator will open where you can choose the file to save to. If you choose an existing file its contents will be overwritten so this feature should be used with caution.

Saving or loading a state space

Instead of computing a state space you can also load a saved state space from a text file. The files must follow the format that is described below. Note that before this option becomes available the corresponding TNCES must have been loaded. To load a state space from a file select the option Load State Space from the State Space menu.

Format of the state space files

The Model Checker application can be used to save a computed state space to a file or load a textual representation of a state space from a file. The format of the files in both cases is similar so that the application is able to load state spaces it has written itself. The format imitates that of the ARC files written by SESA. Therefore files containing the state space representations should have extension '.arc'. The format is described below. The ARC files are text files that begin with an empty row. Below the states and state transitions are described. The states are described with rows of the form 'State nr. N Marking nr. M Clocks nr. C delay = D' where N is the number of the state, M and C are the numbers assigned to the marking and clock values of the state respectively and D is the delay of the state. Note that the Model Checker assigns delay to the post state whereas SESA assigns it to the pre state. Following this line are listed the outgoing state transitions from this state each on a separate line. The lines contain '==' followed by a number representing the duration of the transition, a colon followed by a list of NCES transitions present in the state transition enclosed in brackets ('}'). Finally there is a '=> ' followed by the letter 's' and the number of the post state.

Below is a EBNF representation of the syntax of the ARC files.

The format of ARC files

Since the lines of the files containing state spaces of large systems are bound to become rather long the state space files are rarely readable to a human reader - at least the first section which describes the individual states. For the same reason reading and writing state spaces is impractical for large systems because it takes so long to read and write the files.