- If at any time the condition φ is satisfied then from that point onwards we will surely reach a state where ψ holds.
- If the condition φ is satisfied infinitely often then we will surely reach a state where ψ holds.
| a.(b+τ.c)+τ.a.d | a.(b+τ.c)+τ.a.d+a.b | a.(b+τ.c)+τ.a.d+a.c | a.(b+τ.c)+τ.a.d+a.d |
if $P \mathrel{\mathcal{B}} Q$ and $P \stackrel{\alpha}\longrightarrow P'$,
then there are $Q_0$, $Q_1$, ... , $Q_n$ for some $n \geq 0$,
and $Q'_0$, $Q'_1$, ... , $Q'_m$ for some $m \geq 0$
such that
$Q=Q_0 \stackrel{\tau}\longrightarrow Q_1 \stackrel{\tau}\longrightarrow \dots
\stackrel{\tau}\longrightarrow Q_n \stackrel{(\alpha)}\longrightarrow Q'_0
\stackrel{\tau}\longrightarrow Q'_1 \stackrel{\tau}\longrightarrow \dots
\stackrel{\tau}\longrightarrow Q'_m$,
and moreover $P \mathrel{\mathcal{B}} Q_i$ for all $i=1,...,n$
and $P' \mathrel{\mathcal{B}} Q'_j$ for all $j=0,...,m$.
if $P \mathrel{\mathcal{B}} Q$ and $P \stackrel{\alpha}\longrightarrow P'$,
then there are $Q_0$, $Q_1$, ... , $Q_n$ for some $n \geq 0$,
such that
$Q=Q_0 \stackrel{\tau}\longrightarrow Q_1 \stackrel{\tau}\longrightarrow \dots
\stackrel{\tau}\longrightarrow Q_n \stackrel{(\alpha)}\longrightarrow Q'$,
and moreover $P \mathrel{\mathcal{B}} Q_n$ and $P' \mathrel{\mathcal{B}} Q'$.
Consider a language L without recursion. A different definition of a congruence ~ requires for any $n$-ary operator $f$ of L that
$P_i \sim Q_i$ for $i=1,...,n$ implies $f(P_1,...,P_n) \sim f(Q_1,...,Q_n)$.
Show that this definition is equivalent to the one above.P ~L Q if and only if C[P] ~ C[Q] for any L-context C[ ].
Prove that ~L is the coarsest congruence finer than ~.
Implementation:
(R1 | R2)\$\{$handover$\}$ where
R1 = start.handover.0
R2 = handover.finish.0
|
P --a--> P'
------------------------ (for P' != 0) P;Q --a--> P';Q |
P --a--> 0
---------------- P;Q --a--> Q |
In (a) and (b) below, work with a form of LTS in which any state (possibly with outgoing transitions) can have the label $\surd$. Moreover, the label $\surd$ can occur in a (partial or completed) trace, as explained in the notes.
We assume such an algorithm to be modelled as a Kripke structure. Among the atomic propositions that label the states of this Kripke structure is IntentA, saying that Process A wants to enter the critical section, but has not done so yet. We also have an atomic proposition CritA, stating that Process A is in its critical section. Likewise we have atomic propositions IntentB and CritB.
Click on 'portfolio' in the homework interface,
and select for each of your submitted homeworks 1-10
whether or not you want to include it in your portfolio.
The intention is that you select all homeworks except for one odd-numbered one
and one even-numbered one, but in exceptional cases
you are better off making a different selection.
Your grade is calculated as $n/m$, where $n$ is the total number of points you got for the
homeworks in your portfolio, and $m$ is the maximal number of points you could have gotten
for the homeworks in your portfolio. However, to prevent you from including too few homeworks,
$m$ will never be lower than 235, which is the total points of all homeworks 1-10,
except for the most expensive odd-numbered homework,
and the most expensive even-numbered homework.
This homework question is is about a mutual exclusion algorithm.
The algorithm deals with two concurrent processes A and B that want to alternate critical
and noncritical sections. Each of these processes will stay only a finite amount of time in its
critical section, although it is allowed to stay forever in its noncritical section. It starts in its
noncritical section. The purpose of the algorithm is to ensure that they are never simultaneously
in the critical section, and to guarantee that both processes keep making progress.
$\newcommand{\rA}{{\it readyA}}
\newcommand{\rB}{{\it readyB}}
\newcommand{\tu}{{\it turn}}
\newcommand{\tr}{{\it true}}
\newcommand{\fa}{{\it false}}
\newcommand{\procA}{{\rm A}}
\newcommand{\procB}{{\rm B}}$
The processes use three variables. The Boolean variable $\rA$ can be written by process
A and read by process B, whereas $\rB$ can be written by B and read by A. By setting
$\rA$ to $\tr$, process A signals to process B that it wants to enter the critical section. The
variable $\tu$ is a shared variable: it can be written and read by both processes.
Initially $\rA$ and $\rB$ are both $\fa$ and $\tu = A$.
$\begin{array}{@{}l@{}}
\underline{\bf Process~\procA}\\[.5ex]
{\bf repeat~forever}\\
\left\{\begin{array}{ll}
\ell_1 & {\bf noncritical~section}\\
\ell_2 & \it \rA := \tr \\
\ell_3 & \it \tu := B \\
\ell_4 & {\bf await}\,(\it \rB = \fa \vee \tu = A) \\
\ell_5 & {\bf critical~section}\\
\ell_6 & \it \rA := \fa\\
\end{array}\right.
\end{array}
~~~~~
\begin{array}{@{}l@{}}
\underline{\bf Process~\procB}\\[.5ex]
{\bf repeat~forever}\\
\left\{\begin{array}{ll}
m_1 & {\bf noncritical~section}\\
m_2 & \it \rB := \tr \\
m_3 & \it \tu := A \\
m_4 & {\bf await}\,(\rA = \fa \vee \tu = B) \\
m_5 & {\bf critical~section}\\
m_6 & \it \rB := \fa \\
\end{array}\right.
\end{array}$
Model this protocol (including processes A and B and the three
variables) as a Petri net. You may use actions like CritA
and NonCritB; the actions that manipulate variables can all be
labelled $\tau$. Hint: You may wish to introduce a place for each
of the two values of a Boolean variable.
{$ab, acd, adc, a[cd]$}
Homework 14, Thursday 2-11-2023
(Also due: 7-11-2023 at 10am; accepted without penalty until 8-11-2023 at 10am)
Mid session feedback form, Friday 3-11-2023
Here is a feedback form on this course.
We would appreciate it if you would fill it in.
The identity of submitters is not recorded.
Homework 15, Tuesday 7-11-2023
(Due: 14-11-2023 at 10am; accepted without penalty until 15-11-2023 at 10am)
Homework 16, Thursday 9-11-2023
(Also due: 14-11-2023 at 10am; accepted without penalty until 15-11-2023 at 10am)
Homework 17, Tuesday 14-11-2023
(Due: 21-11-2023 at 10am; accepted without penalty until 22-11-2023 at 10am)
Give a correct structural operational semantics in GSOS format of the sequencing operator.
(A wrong definition already occurred in HW9 Q3.)
Homework 18, Thursday 16-11-2023
(Also due: 21-11-2023 at 10am; accepted without penalty until 22-11-2023 at 10am)
Homework 19, Tuesday 21-11-2023
(Due: 29-11-2023 at 10am; accepted without penalty until 30-11-2023 at 10am)
Homework 20, Thursday 23-11-2023
(Also due: 29-11-2023 at 10am; accepted without penalty until 30-11-2023 at 10am)
Moreover, the choice between b and c should be made only
after execution of a.
Moreover, the choice between $b$ and $c$ should be as late at possible,
so that if either $b$ or $c$ is blocked by the environment, the other one is still possible.
| Rob van Glabbeek | notes | Rob.van.Glabbeek@ed.ac.uk |