% data-primitives.tex -*-latex-*-

% Copyright (C) 2020 Amin Bandali <bandali@uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.


\begin{figure*}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=b]
// textual description
sets and constants:
  A, B: set
  C: subset of A
  c1: a constant of type C
  c2: integer constant with value 3
variables and events:
  v1: powerset of A
  v2: integer
  ev1, ev2: events
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=asmetal]
// AsmetaL
signature:
  enum domain Event = {EV1 | EV2}%*\label{lbl:data/asmetal-event}*)
  abstract domain A%*\label{lbl:data/asmetal-A}*)
  abstract domain B%*\label{lbl:data/asmetal-B}*)
  domain C subsetof A%*\label{lbl:data/asmetal-subsetof}*)
  monitored evs: Powerset(Event)%*\label{lbl:data/asmetal-evs}*)
  controlled v1: Powerset(A)%*\label{lbl:data/asmetal-v1}*)
  controlled v2: Integer%*\label{lbl:data/asmetal-v2}*)
  static c1: C%*\label{lbl:data/asmetal-c1}*)
  static c2: Integer%*\label{lbl:data/asmetal-c2}*)
definitions:
  function c2 = 3%*\label{lbl:data/asmetal-c2-def}*)
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.35\textwidth}
\begin{lstlisting}[style=b]
// B
SETS
  A; B; %* \label{lbl:data/b-parent} *)
  Event = {ev1, ev2}%*\label{lbl:data/b-event}*)
VARIABLES
  v1, v2, evs
CONSTANTS
  isC, c1, c2	 %* \label{lbl:data/b-const1} *)
PROPERTIES
  // subtype predicate
  isC : A --> BOOL &%* \label{lbl:data/b-const2}*)
  c1 : A &
  c2 : INTEGER & c2 = 3
INVARIANT
  v1 : POW(A) &%*\label{lbl:data/b-pow}*)
  v2 : INTEGER &%* \label{lbl:data/b-scalar} *)
  evs : POW(Event)%*\label{lbl:data/b-evs}*)
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.36\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B
CONTEXT
  c0
SETS
  A
  B%*\label{lbl:data/eventb-b}*)
  Event%*\label{lbl:data/eventb-event}*)
CONSTANTS
  C%*\label{lbl:data/eventb-c}*)
  nC%*\label{lbl:data/eventb-nc}*)
  ev1%*\label{lbl:data/eventb-ev1}*)
  ev2%*\label{lbl:data/eventb-ev2}*)
  c1
  c2
AXIOMS
  partition(B, C, nC)%*\label{lbl:data/eventb-part-subtype}*)
  card(C) > 0
  partition(Event, {ev1}, {ev2})%*\label{lbl:data/eventb-part}*)
  c1 : C
  c2 : INT & c2 = 3
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.26\textwidth}
\begin{lstlisting}[style=eventb]
// Event-B (continued)
MACHINE
  m0
SEES
  c0
VARIABLES
  v1
  v2
  evs
INVARIANTS
  v1 : POW(A)%*\label{lbl:data/eventb-pow}*)
  v2 : INT%*\label{lbl:data/eventb-scalar}*)
  evs : POW(Event)%*\label{lbl:data/eventb-evs}*)
\end{lstlisting}
\end{minipage}
%
\caption{Primitives in snapshot declarations across languages (part
  one)}
\label{fig:data/primitives}
\end{figure*}
% --------------------------------------------------------------------
\begin{figure*}
%
\ContinuedFloat
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=alloy]
// Alloy
sig A, B {}
sig C extends A%*\label{lbl:data/alloy-subtype}*)
enum Event { ev1, ev2 }%*\label{lbl:data/alloy-enum}*)
sig Const {%*\label{lbl:data/alloy-const-start}*)
  c1: one C,
  c2: one Int
} { c2 = 3 }%*\label{lbl:data/alloy-const-end}*)%*\label{lbl:data/alloy-const-fact}*)
sig Example {
  v1: set A,%*\label{lbl:data/alloy-v1}*)
  v2: one Int,%*\label{lbl:data/alloy-v2}*)
  evs: set Event%*\label{lbl:data/alloy-evs}*)
}
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=dash]
// Dash
open util/integer
sig A, B {} %* \label{lbl:data/dash-sig} *)
sig C extends A {}%* \label{lbl:data/dash-subtype} *)
sig Const {%*\label{lbl:data/dash-const-start}*)
  c1: one C,
  c2: one Int
}%*\label{lbl:data/dash-const-end}*)
state Example {
  v1: set A, %* \label{lbl:data/dash-set} *)
  v2: one Int, %* \label{lbl:data/dash-singleton} *)
  event ev1 {} %*\label{lbl:data/dash-ev1}*)
  event ev2 {} %*\label{lbl:data/dash-ev2}*)
  invariant { Const.c2 = 3 }%*\label{lbl:data/dash-const-inv}*)
}
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=tla]
\* TLA+
EXTENDS Integers, FiniteSets
CONSTANTS A, B, C, c1, c2
VARIABLES v1, v2, evs

Event == {"ev1", "ev2"}%*\label{lbl:data/tla-enum}*)

TypeOK ==
  /\ v1 \in SUBSET A
  /\ v2 \in Singleton(Int)%*\label{lbl:data/tla-scalar}*)
  /\ evs \in SUBSET Event%*\label{lbl:data/tla-subset}*)
  /\ c1 \in C
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=pluscal]
\* PlusCal
EXTENDS Integers, FiniteSets
CONSTANTS A, B, C, c1

(* --algorithm example
variables v1, v2, evs;

define
c2 == 3
\* helper predicate
Singleton(S) == {{i} : i \in S}
Event == {"ev1", "ev2"}

TypeOK ==
  /\ v1 \in SUBSET A
  /\ v2 \in Singleton(Int)
  /\ evs \in SUBSET Event
  /\ c1 \in C
  /\ c2 \in Int
end define
end algorithm *)
\end{lstlisting}
\end{minipage}
%
\caption{Primitives in snapshot declarations across languages (part two)}
\end{figure*}


%% Local Variables:
%% tex-main-file: "../bandali-mmath-thesis.tex"
%% End:
