crestdsl.verification package¶

Verifiable Properties (Checks)
Convenience API
Expert Model Checking API
- TCTL API

Verifiable Properties (Checks)¶

crestdsl.verification.check(arg)¶

Use this function to create a Check object. Checks are the basic form of verifiable properties. There are two types of checks, state checks and port checks. State checks assert that an entity is in a given state, port checks compare the value of a port to a constant or another port.

Use check(entity) == entity.stateA to create a state check, for instance.

Port checks are created using check(entity.port) <= 33 or `check(entity.port) != another.port

You can also combine these atomic checks to larger ones. The operators are: - conjunction (and): & - disjunction (or): | - negation (not): -

Parameters: arg (Entity or Port) – If you pass an entity, a StateCheck will be returned. If you pass in a Port, the function will create a PortCheck.
Returns: depending on what you put in, you will receive either a StateCheck or a PortCheck
Return type: StateCheck or PortCheck

Examples

>>> state_chk = check(entity) == entity.my_state
>>> port_chk = check(entity.port) == 33
>>> and_chk = state_chk & port_chk
>>> or_chk = state_chk | port_chk
>>> not_chk = -state_chk

Convenience API ¶

crestdsl.verification.after(time)¶

Initialises a Verifier that will test if formula is valid after a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. after(30) states that the formula has to hold after 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.before(time)¶

Initialises a Verifier that will test if formula is valid before a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. before(30) states that the formula has to hold in the initial 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.is_possible(check)¶

Test if it is possible to reach a system configuration described by check.

The TCTL formula will be EF(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.always(check)¶

Test if every reachable a system configuration satisfies the check.

The TCTL formula will be AG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.always_possible(check, within=None)¶

Test if it is always possible to reach a system configuration described by check.

Parameters

check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
within (numeric) – If specified, tests if the state can always be reached within a certain maximum time span. For example “Can we always raise the temperature within 30 minutes”.

Returns

The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.

Return type

Verifier

crestdsl.verification.never(check)¶

Test if a system configuration that adheres to``check`` can never be reached.

The TCTL formula will be AG(Not(check))

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

crestdsl.verification.forever(check)¶

Test if there is one path where every state satisfies check.

The TCTL formula will be EG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

class crestdsl.verification.Verifier(system=None)¶

This class hosts the functionality for the verification API.

Notes

You shouldn’t create a Verifier object directly. Use the convenience API methods instead (e.g. ispossible() or always()).

after(time)¶

after(time)

Initialises a Verifier that will test if formula is valid after a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. after(30) states that the formula has to hold after 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

always(check)¶

always(check)

Test if every reachable a system configuration satisfies the check.

The TCTL formula will be AG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

always_possible(check, within=None)¶

always_possible(check, within=None)

Test if it is always possible to reach a system configuration described by check.

Parameters

check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
within (numeric) – If specified, tests if the state can always be reached within a certain maximum time span. For example “Can we always raise the temperature within 30 minutes”.

Returns

The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.

Return type

Verifier

before(time)¶

before(time)

Initialises a Verifier that will test if formula is valid before a certain amount time has passed.

Parameters: time (numeric) – Sets the lower barrier of the interval to be tested. e.g. before(30) states that the formula has to hold in the initial 30 time units.
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

check(draw_result=False)¶

Triggers the verification. This includes the compiling the tctl formula, explorating the statespace and then checking the formula on the statespace.

Parameters: draw_result (bool) – The verifier can draw the statespace and highlight the nodes that satisfy the formula. This is VERY slow though. So don’t run it if the statespace is bigger than a few dozen nodes.
Returns: The result of the model checking. I.e. if the formula holds on the root state of the state space.
Return type: bool

forever(check)¶

forever(check)

Test if there is one path where every state satisfies check.

The TCTL formula will be EG(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

property formula¶: The current formula (as TCTL object).

is_possible(check)¶

is_possible(check)

Test if it is possible to reach a system configuration described by check.

The TCTL formula will be EF(check)

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

never(check)¶

never(check)

Test if a system configuration that adheres to``check`` can never be reached.

The TCTL formula will be AG(Not(check))

Parameters: check (Check) – The property to test for. Use crestdsl.verification.check() to specify the property (e.g. check(my_system.output) > 300)
Returns: The verifier object, which can be further customised. Verification can be triggered by running the Verifier’s check() method.
Return type: Verifier

Expert Model Checking API ¶

class crestdsl.verification.StateSpace(system=None, *args, **kwargs)¶

Creates a graph of initial node + stabilised nodes. Graph elements are SystemState objects.

This class is based on networkx.DiGraph. See networkx documentation for more info.

calculate_successors_for_node(ssnode)¶: CAREFUL!! this is the one where we only do one at a time! BUT: it’s faster than executing the parallel one on one thread

explore(iterations_left=1, iteration_counter=1, parallel=False)¶

Asserts that the graph is expanded so all paths have a minimum length i.e. the length to the leaves is at least a amount

Parameters

iterations_left (int) – How many iterations of exploration should be done (or None for “inifitely many”)
iteration_counter (int) – Don’t specify it. It’s for logging purposes only.
parallel (bool) – Unstable. Don’t use it!

explore_until_time(time)¶

Asserts that the graph is expanded so all paths have a minimum length i.e. the length to the leaves is at least a amount

Parameters: time (numeric) – The minimum length of all paths between root and the nodes

class crestdsl.verification.ModelChecker(statespace=None)¶

Create a ModelChecker that can explore a StateSpace. Use check() to trigger the exploration.

__init__(statespace=None)¶

Parameters: statespace (StateSpace) – The statespace (timed Kripke structure) that will be explored.

check(formula, systemstate=None)¶

Trigger the model checking implementation.

Parameters

formula (TCTLFormula) – A tctl formula object that specifies the property that should be checked.
systemstate (SystemState) – In case you want to execute the formula on a different state than the statespace’s root.

Returns

The result of the model checking. I.e. if the formula is satisfied.

Return type

bool

TCTL API ¶

class crestdsl.verification.tctl.Interval(start=0, end=inf, start_op=<built-in function ge>, end_op=<built-in function lt>)¶

Define an interval for the timed versions of the TCTL operators.

Use comparison operators (<, >, <=, >=, ==) to specify the bounds of the interval. Note, that you can only apply one operator at a time. (Use parenthesis!)

Examples

>>> intvl = Interval()  # [0, ∞)
>>> intvl2 = Interval() > 33  # (33, ∞)
>>> intvl3 = Interval() <= 42  # [0, 42]
>>> invtl4 = Interval() == 100  # [100, 100]
>>> invtl5 = (Interval() > 12) < 48  # (12, 48)

ends_before(value)¶

Test if the interval ends before a certain time.

Parameters: value (numeric) – The value you want to test.

ininterval(value)¶

Test if a value is inside the interval.

Parameters: value (numeric) – The value you want to test.

is_after(value)¶

Test if the interval starts after a certain time.

Parameters: value (numeric) – The value you want to test.

is_before(value)¶

Test if the interval ends before a certain time.

Parameters: value (numeric) – The value you want to test.

starts_after(value)¶

Test if the interval starts after a certain time.

Parameters: value (numeric) – The value you want to test.

starts_at(value)¶

Test if the interval starts at a certain time.

Parameters: value (numeric) – The value you want to test.

starts_at_or_after(value)¶

Test if the interval starts at or after a certain time.

Parameters: value (numeric) – The value you want to test.

class crestdsl.verification.tctl.TCTLFormula(formula)¶: The base class of all TCTL formulas. Don’t use it!

class crestdsl.verification.tctl.Not(formula)¶

__init__(formula)¶

Parameters: formula (TCTLFormula) – A TCTL subformula (either another TCTLFormula or a Check)

class crestdsl.verification.tctl.And(phi, psi)¶

__init__(phi, psi)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)

class crestdsl.verification.tctl.Or(phi, psi)¶

__init__(phi, psi)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)

class crestdsl.verification.tctl.Implies(formula)¶

__init__(formula)¶

Parameters: formula (TCTLFormula) – A TCTL subformula (either another TCTLFormula or a Check)

class crestdsl.verification.tctl.Equality(formula)¶

__init__(formula)¶

Parameters: formula (TCTLFormula) – A TCTL subformula (either another TCTLFormula or a Check)

class crestdsl.verification.tctl.EU(phi, psi, interval=None)¶

__init__(phi, psi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.EF(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.EG(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.AU(phi, psi, interval=None)¶

__init__(phi, psi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
psi – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.AF(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

class crestdsl.verification.tctl.AG(phi, interval=None)¶

__init__(phi, interval=None)¶

Parameters

psi (TCTLFormula) – A TCTLFormula or Check (state or port check)
interval (Interval) – The interval of the timed operator

crestdsl.verification package¶

Verifiable Properties (Checks)¶

Convenience API¶

Expert Model Checking API¶

TCTL API¶

Convenience API ¶

Expert Model Checking API ¶

TCTL API ¶