Tutorial 1: 9th October 2019 Flashcards
PROMELA, Spin, and Labelled Transition Systems
How can you represent “if not p then p is never true”?
¬p → □ (¬p)
or □ (¬p → ¬◇p)
How can you check an eventually property without a lebelled end?
Have 2 loops. In the first loop, loop until the variable is acceptable, after which break and go to the second loop. In the second loop, loop until the variable is not acceptable, at which point break out. This would terminate the never claim, so the property fails.
How can you check the value of a variable at the start of a Spin execution with a never claim?
Just put the value and its non-desired value in the claim, since never blocks always execute first, before any processes.
How do you formally define Transition Systems?
Transition Systems are defined as (S, Act, T, I, AP, L)
where
S = finite set of states Act = finite set of actions: ~ inputs T = set of transitions, in form T ⊆ (S x Act x S): which state to go to from a current state for a given action I = set of initial states AP = set of atomic propositions L = labelling function: determines which APs hold in which states
What is the difference between an AP-deterministic and action-deterministic TS?
AP-deterministic and action-deterministic TSes both have ⩽ 1 start state.
Action-deterministic TSes have ⩽ 1 successor they can transition to
States in AP-deterministic TSes have ⩽ 1 successor they can transition to that satisfy an AP, for each possible pair of each state and an AP in the set of all APs
What is a trace?
Trace = trace of execution = the chronological list of states of an execution of a model up to a certain point.
How do you notate propositions, states, and whole specs?
How do traces and propositions relate?
How do specs and traces relate?
How can you assess the possibility of APs with this notation?
proposition i = pi
state i = si
trace i = ti
SPEC = all traces, ti, for a given specification.
tx ⊨ p if trace x satisfies AP p in initial state/s of tx
tx ⊨ ◇p if trace x satisfies AP p in initial state/s of tx
tx ⊭ p if trace x does not satisfy AP p in initial state/s of tx
SPEC ⊨ p if all its traces satisfy p in their initial states
If any tx ⊭ p then SPEC ⊭ p
Can notate possibility with negation: SPEC ⊨ ¬p
if this fails then ∃ a trace ti in SPEC for which ti ⊨ p
What are program graphs?
Program graphs are a graphical representation of a program’s source code. For Spin models, the nodes of the program graph represent the states and the edges represent the program’s transitions between them. States will have code fragments to execute.
How can you represent a program graph in a pictorial manner?
Draw a graph for each process. In each processes’ graph, make states for each node, and label them with the value of global variables (at the start). Make edges for each transition, and label them with the action to trigger them.
What does the ||| operation do?
Complete interleaving.
How can you determine the reachable part of TSes?
Draw a program graph and find those with no execution path from the root - start state. (?)
What does Spin use for its underlying system representation and execution?
labelled transition systems
What is a Transition System?
A theoretical state machine often used for describing the potential behaviour of discrete systems (i.e. systems with more than one state).
What is a Labelled Transition System?
Labelled TSes include labels: short representations of conditions for transitions (usually) or actions performed during them.
