crestdsl.simulation package

The simulation package contains everything that’s required for the simulation of crestdsl systems.

crestdsl provides in fact several simulator implementations for the exploration of model evolution. They mostly provide the same API and functionality and differ in minor details of the implementation. Below, three of them are presented. Their difference lies in the way they deal with non-determinism. CREST systems can be non-deterministic if two or more transitions are enabled from the same, currently active state. Despite the fact that non-determinism is a vital aspect of CREST to model the random execution, it is of high interest to also support its resolution and manual selection of the transition to follow, e.g. for the deliberate exploration of specific system behaviour. The dealing with such non-determinism is the discriminating difference between the individual simulators.

The three simulator implementations treat such non-determinism as follows:

1. The first implementation, the most basic CREST simulator (Simulator), randomly chooses one enabled transition when it encounters non-determinism. It thus strictly follows the basic CREST semantics. This system is useful for initial explorations in non-deterministic models (e.g. to get a feeling for possible behaviour scenarios) and for general simulation of deterministic models.

2. Secondly, the InteractiveSimulator is used when it comes to manual exploration of a non-deterministic model. Anytime a situation with multiple enabled transitions is encountered, the simulator stops and prompts the user to make a choice. Evidently, this feature is meant for the exploration of smaller models, where such situations rarely occur. For highly non-deterministic models this form of exploration can become tedious.

3. The third simulator is the PlanSimulator. It can be used for the programmatic simulation of a system trace. The simulation is launched with a list of commands that helps to orchestrate the execution. The command list contains information about advance and port setting actions. Additionally, the ports can specify which transition to take, in case non-determinism is encountered. Thus, the PlanSimulator can be even used to precisely specify a certain system evolution and chosen behaviour. This capacity is highly useful for unit testing or the analysis of specific execution schedules. The specification of large execution plans can quickly become overwhelming, especially for large systems. Usually, execution plans are therefore machine generated, e.g. in combination with a state space exploration or formal verification scenario.

Note

This text is based on a part of Stefan Klikovits’s PhD Thesis [Kli19].

class crestdsl.simulation.Simulator(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)

The vanilla crestdsl simulator. It offers APIs to stabilise a system and advance time.

Additionally, there are shortcuts to get the execution trace and to plot the system.

__init__(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)

Create a new simulator object. In most cases you will only need ot declare the first system parameter.

All other parameters are rarely needed.

Parameters

  • system (Entity) – The system/entity whose evlution should be simulated

  • timeunit (crestdsl.model.REAL or crestdsl.model.INT) – Set this to decide whether the next transition time should be precise or round up to the next integer.

  • plotter (crestdsl.ui.elk or crestdsl.ui.dotter) – Modify the library that this simulator uses for drawing CREST diagrams.

  • default_to_integer_real (bool) – Should the SMT solver use INTEGER and REAL theories when encountering int/float datatypes (unless otherwise specified)?

  • record_traces (bool) – You can deactivate the recording of trace data. (Slightly more performance/memory friendly, although usually you wouldn’t notice.)

  • own_context (bool) – DON’T USE THIS! It’s a preliminary switch that should enable parallel execution at some point in the future.

  • max_step_size (numeric value) – This will only ever advance in steps of a certain maximum size. You can use it to increase the amount of trace data. Can also be useful for non-linear systems. (Although they aren’t really supported by crestdsl anyway)

system

A handle to the system that is being simulated. You can use it to e.g. modify input values

stabilise()

Stabilise the system. This includes propagation of all port values through influences and updates, then triggering any enabled transitions, then doing propagation again, and transitions, and … until a fixpoint is reached.

Warning

This can result in an infinite loop if your system has a cycle of enabled transitions.

stabilize()

For all the Americans out there. Does the same thing as stabilise().

advance(time_to_advance, consider_behaviour_changes=True)

Advance a certain amount of time in your system.

Parameters

  • time_to_advance (numeric) – The time advance that should be simulated

  • consider_behaviour_changes (bool) – You usually won’t have to modify this (so don’t!) Allows you to deactivate searching for if/else condition changes. It will be removed soon anyway!

advance_to_behaviour_change(consider_behaviour_changes=True)

Calculates when the next discrete change in behaviour will happen and advance as many time units. Note, this also does the according stabilisation, so you cannot stop “before” the behaviour change.

Parameters

consider_behaviour_changes (bool) – You usually won’t have to modify this (so don’t!) Allows you to deactivate searching for if/else condition changes. It will be removed soon anyway!

next_behaviour_change_time(excludes=None)

Calculates when the next discrete change in behaviour will happen.

Parameters

excludes (list of objects) – If you don’t care about behaviour changes in certain objects, use excludes to ignore them. Don’t use it unless you know what you’re doing!

Returns

Returns a tuple of (numeric, object) that states when the next behaviour change will happen (in time units), and in which object it will happen (i.e. a transition, update or influence)

Return type

tuple

trace

A handle to the TraceStore object that holds the ports values and states.

global_time

Return the global time value (i.e. the sum of all time advances)

plot(entity=None, **kwargs)

Create a drawing of the system. Uses the default plotter defined in the Config unless you specified a different library when you initialised.

Parameters

  • entity (Entity) – If you wish to plot something else than the simulator’s system. (Why would you, though?!)

  • kwargs (dict) – Anything defined as keyword argument will be passed on to the plotting library. This way you can parameterise things.

class crestdsl.simulation.InteractiveSimulator(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)

Bases: crestdsl.simulation.simulator.Simulator

This is a simulator will stop every time two transitions are enabled in the same entity at the same time and prompt the user for what to do.

Next to choosing a transition,uUsers can perform various actions (e.g. inspect variables, plot the system or stop the simulation.

class crestdsl.simulation.PlanSimulator(system, timeunit=<Types.REAL: 'real'>, plotter=<module 'crestdsl.ui.dotter' from '/home/docs/checkouts/readthedocs.org/user_builds/crestdsl/checkouts/latest/crestdsl/ui/dotter.py'>, default_to_integer_real=True, record_traces=True, own_context=False, max_step_size=inf)

Bases: crestdsl.simulation.simulator.Simulator

The PlanSimulator offers the same interface as the usual Simulator. However, it additionally allows the triggering of an execution_plan in the run_plan() method.

run_plan(execution_plan)

Executes a plan. The execution plan is a heterogeneous list of the following items:

  • numeric values: (specify time advances)

  • pairs of (numeric, {entity: transition}-dict): advance a certain time and choose transition, everytime non-determinism is encountered in entity

  • {port: value} dicts (for setting of input ports)

  • {entity: transitions} dicts (for resolving conflicts)

The list items will be iteratively consumed. If errors are observed they raise ValueError exceptions.

If there is non-determinism, but no dict specifies how to resolve it, then we fall back to randomness.

Here’s a documented example of a plan: [

# advance 10 time units: 10,

# set values: {entity.port : 33, entity.port2: -200}, # advance 20 time units and choose these transitions everytime there is a conflict in this period (20, {entity: entity.transition1, entity.subentity: entity.subentity.transition2} ),

# advance 33 time units. # When you hit a conflict, check if the first element is an entity-state dict # if the entity is a key in the first element, then pop it and # use it to reolve the conflict (otherwise choose randomly) # then continue until anothoer conflict or end of advance 33, {entity: entity.transitionA}, {entity: entity.transitionB}, {entity: entity.transitionA},

# if you have two entities and you don’t know which one will be conflicting first # (because they’ll have conflicts at the same time) # you can put them both in a dict and duplicate the dict. # the first one will pop the first dict, the second one the second dict:

444, {entity.subentity1: entity.subentity2.transA, entity.subentity2: entity.subentity2.transB}, {entity.subentity1: entity.subentity2.transA, entity.subentity2: entity.subentity2.transB},

]

Parameters

execution_plan (list) – The list of instructions that should be executed.

Raises

ValueError – In case there is something wrongly specified (e.g. take a transition that is not enabled, or so)