crestdsl.verification package¶
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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()
oralways()
).-
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
-
-
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
-
-
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
-
-
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
-
-
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
-
-
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
-
-
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
-
-
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
. Usecheck()
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
-