Title: Theory / Unimportant / CS / Fundamental / Model Checking / (Principles of) - Baier, Katoen{
Tags: fromAlgorithm hasNotNewEffectReturnsMeaning oldAlgoNewName some_instruction

Name: The state graph of \(TS\)
Definition: \((S,\{(s,s')\in S^2\mid s'\in Post(s)\})\)
Page: 95
Chapter: 3
Section: 2.1
Variables: \(TS=(S,act,\to,I,AP, L)\) a TS
Notation: \(G(TS)\)

Page: 47, 67
Implementation: do :: true ⇒ skip;
atomic{b 1 := true; x := 2};
if :: (x = 1) ∨ ¬b 2 ⇒ crit 1 := true fi
atomic{crit 1 := false; b 1 := false}
od
\(w\) for wait,
\(c\) for critical
\(n\) for noncritical
Section: 2.2, 2.5
Chapter: 2
Effect: Ensure that \(c_1\) and \(c_2\) never holds simultaneously,
each request is eventually satisfied (assuming the critical section is left)
Name: Peterson mutual exclusion algorithm
Context: Promela
Index: 10
Kind: Fig,