Experiment File Format

For example experiments see the experiments directory.

Main Experiment File

This file contains path to all files constituting an experiment and other settings. Paths are always considered relative to the experiment file.

experiment.properties:

sbml.file=<path>
stl.file=<path>
space.initial.file=<path>
space.simulation.file=<path>
simulation.precision.file=<path>
result.output.file=<path>
timeout.amount=<number of time units>
timeout.unit=<seconds|minutes|hours|days>
iteration-limit=<number of iterations>

For the experiment to run, files specified in paths have to exist and be correct. The exception is result.output.file, which is generated by parasim.

The model itself is referenced as sbml.file and you can generate it using your favourite sbml editor.

When you have only SBML file containing model description, you may use convenience bash script initialize-experiment.sh to create an experiment from this file. For invocation and options execute initialize-experiment.sh -h.

STL Formula File

This file contains an STL formula whose robustness is computed. It is an XML file which conforms to the following XML schema. In the main experiment file it is referred to as stl.file.

The formula itself is built inductively and enclosed in:

<formula xmlns="http://www.sybila.org/parasim/stl-formula">
    <!-- formula itself -->
</formula>

Atomic Propositions

Atomic propostitions are linear conditions over model variables in the format C1*X1+...+Cn*Xn>B where C1,...,Cn,B are real constants and X1,...,Xn are model variables (as defined in SBML file). Such atomic proposition is encoded:

<predicate>
    <variable multiplier="C1"><!-- X1 name --></variable>
    <!-- ... --> 
    <variable multiplier="Cn"><!-- Xn name --></variable>
    <greater/>
    <value><!-- B --></value>
</predicate>

In addition to > (<greater/>), = (<equals/>) and < (<lesser/>) relations are allowed.

Boolean Operators

• and

<and>
    <!-- formula -->
    <!-- formula -->
</and>

• or

<or>
    <!-- formula -->
    <!-- formula -->
</or>

• not

<not>
    <!-- formula -->
</not>

Temporal Operators

STL does not allow Next operator. Furthemore, each temporal operator has a time interval (note that only closed interval are allowed):

<interval>
    <lower type="closed"><!-- lower bound --></lower>
    <upper type="closed"><!-- upper bound --></upper>
</interval>

• until

<until>
    <!-- interval -->
    <!-- formula: initial condition -->
    <!-- formula: release -->
</until>

• globally

<globally>
    <!-- interval -->
    <!-- formula -->
</globally>

• future

<future>
    <!-- interval -->
    <!-- formula -->
</future>

Space File

Space file defines a multi-dimensional space. There are two space files referred to in the main experiment file:

• space.initial.file -- space of initial conditions (which is sampled according to density.sampling.file -- see below)
• space.simulation.file -- space of simulation: when a simulated trajectory leaves this space, it is truncated

Both have the same format -- XML conforming to the following schema.

Each space is defined as a product of real (floating point) intervals (i.e. it is bounded in each dimension). The resulting format is:

<space xmlns="http://www.sybila.org/parasim/space">
    <time min="simulation start time" max="simulation end time"/><!-- this line is obligatory only for space.simulation.file -->
    <variable name="variable-name" min="lower bound" max="upper bound"/>
    <parameter name="parameter-name" min="lower bound" max="upper bound"/>
    <!-- other variables/parameters -->
</space>

Simulation Precision Settings

The precision of simulation is set in simulation.precision.file. This is an XML file conforming to the following XML Schema. It specifies time step of simulation, maximum relative error and maximum absolute errors in each dimension.

<precision xmlns="http://www.sybila.org/parasim/precision" maxRelativeError="maximum relative error" timeStep="simulation time step">
    <dimension maxAbsoluteError="maximum absolute error in the fisrt model species"/>
    <!-- more dimensions -->
</precision>

Typically, maximum relative error is non-zero and maximum absolute errors are set to zero.

Result File

This file contains result of verification executed by parasim. It is referred to as result.output.file in the main experiment file, it is an XML file conforming to the following schema.

A result consists of individual points whose robustness was computed. Each point has its coordinates (in all dimensions) and robustness value. The resulting format is:

<result xmlns="http://www.sybila.org/parasim/verification-result">
    <point>
        <dim><!-- coordinate in the first dimension --></dim>
        <!-- coordinates in another dimensions -->
        <robustness><!-- robustness value --></robusntess>
    </point>
    <!-- another points -->
</result>