Assignment 2; \next command

2 files changed, 81 insertions, 1 deletions

diff --git a/assignment2.tex b/assignment2.tex
new file mode 100644
index 0000000..0b82ded
--- /dev/null
+++ b/assignment2.tex
@@ -0,0 +1,46 @@
+\documentclass[a4paper]{article}
+
+\usepackage{geometry}
+\usepackage[english]{babel}
+
+\usepackage{enumitem}
+\setenumerate[1]{label=\alph*)}
+
+\usepackage{fancyhdr}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}
+\fancyhead{}
+\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
+\pagestyle{fancy}
+
+\usepackage{sv}
+
+\title{Software Verification - assignment 2}
+\author{Camil Staps}
+
+\def\run#1{\mathit{run}_{#1}}
+\def\stop#1{\mathit{stop}_{#1}}
+
+\begin{document}
+
+\maketitle
+\thispagestyle{fancy}
+
+\setcounter{section}{2}
+\section{CTL-properties of processes}
+
+\begin{enumerate}
+    \item $\invariantly(\lnot(\run1\land\run2))$.
+    \item $\potentially(\run1\land\run2)$.
+    \item $\inevitably\eventually(\run1)$.
+    \item $\potentially\eventually(\run1)$.
+    \item $(\potentially(\lnot\run1\until\run2)) \land (\potentially(\lnot\run2\until\run1))$.
+    \item Impossible: `never' cannot be expressed in CTL: does it mean `in no case whatsoever can this happen' or `there is a path for which this never happens'? But in LTL: $(\always\lnot\run2)\then(\always\run1)$.
+    \item For the same reason as above we cannot express this in CTL. We cannot express this in LTL either, because `may \dots forever' can only be expressed in CTL.
+    \item $\invariantly\exists\next\stop{i}$ with $i\in\{1,2\}$.
+    \item $\invariantly((\forall\lnot\stop1)\then\inevitably\run1)$.
+    \item $\invariantly(\lnot\run1\then\potentially(\lnot\run1\untilW\run2))$.
+\end{enumerate}
+
+\end{document}
+
diff --git a/sv.sty b/sv.sty
index ed9dd0a..d28ca47 100644
--- a/sv.sty
+++ b/sv.sty
@@ -3,6 +3,40 @@
 \let\eventually\lozenge
 \let\always\square
 \def\until{\mathop{\mathsf U}}
-\let\next\bigcirc
+\def\untilW{\mathop{\mathsf W}}
 
 \let\then\Rightarrow
+
+\def\potentially{\exists\eventually}
+\def\inevitably{\forall\eventually}
+\def\potentiallyalways{\exists\always}
+\def\invariantly{\forall\always}
+
+% The below is taken from the circle package; https://www.ctan.org/pkg/circle
+% However, circle is not available in texlive, so this is easier.
+\newcommand*\Circle[1][n]{%
+  \mathchoice{\@Circle{#1}{\tf@size}}{\@Circle{#1}{\tf@size}}%
+             {\@Circle{#1}{\sf@size}}{\@Circle{#1}{\ssf@size}}%
+}
+
+% Bugs: circles have size n at fontsize 2n-1 and 2n; they do not scale linearly
+%       depending on the fontsize
+
+\newcommand*\@Circle[2]{{%
+  \dimen0=#2pt \advance\dimen0by4.5pt \dimen1=1pt \divide\dimen0by\dimen1
+  \count255=\dimen0 \ifodd\count255 \advance\count255by1 \fi\divide\count255by2
+  \ifnum\count255=0 {}\else\ifnum\count255>15 {}\else
+    \dimen0=\count255pt
+    \edef\circfont{tencirc\ifnum\count255>8 w\fi}
+    \advance\count255by\if #1f111\else 95\fi
+    \dimen2=.82\dimen0 \advance\dimen2by.4pt
+    \raisebox{.5\dimen0}[\dimen2]{\makebox[1.2\dimen0]{%
+      \hspace*{.9\dimen0}%
+      \csname\circfont\endcsname
+      \char\count255 %
+    }}%
+  \fi\fi
+}}
+
+\let\next\Circle
+