This sets the working directory natively, which is used to read or
write files specified with relative locations. For example:
prism -dir /some/dir model.prism model.props
is the same as:
prism /some/dir/model.prism /some/dir/model.props
Exported files also go to the same directory.
The same applies when passing model/property files to the GUI via
the command-line and when specifying export filenames as options.
The GUI file chooser is also initialised to the -dir location.
This can be used where an exact result for testing is not known,
but bounds have been obtained, e.g., via interval iteration.
The bounds a and b must be doubles. As usual, no spaces are allowed.
Code is split into different methods for each type of test.
It is also mostly relocated to a new class prism.ResultTesting,
since it should not really be tied to the Property object.
The result for testing can now be passed as a Result object,
as well as Double, Integer, etc., with the former being preferred.
This will allow info attached to the Result object to be used
for the correctness, notably accuracy/error info.
Also add a new testing regression test - just some constants,
including border cases - infinity, NaN, etc.
Was already enabled for steady-state probabilities in 3cb4f42d,
following addition of no-sparse printing for MTBDD vectors.
Not sure why this was not enabled too.
Was previously being parsed as a PRISM expression as a fallback,
but the parser currently does not handle big integers.
Test case added. And these tests moved to a new "testing" directory.
Like --args <file>, this allow a list of lists of arguments to be provided,
with each element of the outer list representing a separate run of PRISM
to be performed on all benchmarks. Here, these can be provided directly
on the command-line, as a comma-separated list, rather than creating a file.
For example:
prism-auto ... --args-list '-gs,-jac,-jor -omega 0.9'
The prism-log-extract script extracts and collates info from a
collection of PRISM log files.
The basic usage is "prism-log-extract <targets>" where <targets>
is one or more log files or directories containing log files.
The default behaviour is to extract all known fields from all logs
and then print the resulting table of values in CSV format.
Run "prism-log-extract --help" for details of further options.
New switch --filter-models X which restricts the list of models used from
a directory to those that match the filter X. Currently, this can refer to
the number of states and/or the model type. Examples:
* prism-auto . --filter-models "states>100 and states<10000"
* prism-auto . --filter-models "model_type=='DTMC'"
* prism-auto . --filter-models "'MC' in model_type"
The model metadata is by default read in from a models.csv file (as found,
for example, in the PRISM benchmark suite). The name of the file used can
be changed with --models-info FILE.
When using the -l (--log) option and also the -a (--args) option,
subirectories are created for each entry in the args file.
This makes it easier to process the log files afterwards.
Relatedly, if the directory specified in the -l switch, or the required
subdirectories, do not exist, there is now no error and they are created.
Dave Parker