Week 3: Promela II Flashcards
In which two categories do the properties of LTL fall?
- Safety properties
- Liveness properties
What do safety properties specify?
That something bad never happens
What do liveness properties specify?
That something good eventually happens
In which way are the Symbolic names (introduced through mtype) numbered?
In reverse order of their definition declarations
What does the typedef declarator do?
Creates user-defined types
What are the two rules for typedef?
- They cannot be self-referential
- They must be global
What is _pid?
It is a pre-defined, local, read-only variable of type pid that carries the unique ID of a process
What is the value of _pid of init?
0
What does the run primitive do?
Dynamically creates new instances of processes (defined using proctype) during the execution of the model.
What does the assert statement accept as input?
An invariant
What is an invariant?
A condition that must remain true throughout the entire system
What happens when an invariant is evaluated as false?
The execution of the assert statement reports a violation of the invariant, and system execution terminates.
What needs to be done to ensure the invariant is interleaved with the execution of other statements from other processes?
The assert statement has to be entered in its own process
What is the advantage of placing the assert statement in its own process?
System-wide non-determinism
What is the disadvantage of assertions?
They don’t check invariants exhaustively
