% data-cons-mult.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.44\textwidth}
\begin{lstlisting}[style=b]
// textual description
uninterpreted sets from Figure 6.1
snapshot variables:
  f1: total function from A to B
  f2: monitored surjective function from A to B
  R1: 1-to-2 binary relation from C to B
  s1: sequence of A's
\end{lstlisting}
%
\begin{lstlisting}[style=b]
// B
VARIABLES
	f1, f2, R1, s1
INVARIANT
	f1 : A --> B  &%*\label{lbl:data/b-f1}*)
	f2 : A -->> B &%*\label{lbl:data/b-f2}*)
	R1 : A * B    &%*\label{lbl:data/b-R1}*)
	s1 : seq(A)   &%*\label{lbl:data/b-s1}*)
	!(v).(v: A & isC(v) <=> %* \label{lbl:data/b-mult-start} *)
		card(R1(v)) = 2 &
		not(isC(v)) => card(R1(v)) = 0)%* \label{lbl:data/b-mult-end} *)
\end{lstlisting}
%
\begin{lstlisting}[style=eventb]
// Event-B
MACHINE
  m0
SEES
  c0
VARIABLES
  f1
  f2
  R1
  s1
INVARIANTS
  f1 : A --> B%*\label{lbl:data/eventb-f1}*)
  f2 : A -->> B%*\label{lbl:data/eventb-f2}*)
  R1 : C <-> B%*\label{lbl:data/eventb-R1}*)
  s1 : NAT +-> A%*\label{lbl:data/eventb-s1}*)
  !v . v : C =>%*\label{lbl:data/eventb-R1-start}*)
    (card({v} <| R1) = 1 &
     card(R1[ {v} ]) = 2)%*\label{lbl:data/eventb-R1-end}*)
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.55\textwidth}
\begin{lstlisting}[style=asmetal]
// AsmetaL
signature:
	controlled f1: Powerset(Prod(A, B))%*\label{lbl:data/asmetal-fr-start}*)
	monitored  f2: Powerset(Prod(A, B))
	controlled r1: Powerset(Prod(C, B))%*\label{lbl:data/asmetal-fr-end}*)
	controlled s1: Seq(A)
	derived isfun: Powerset(Prod(D1, D2)) -> Boolean
	derived issurfun: Powerset(Prod(D1, D2)) -> Boolean
	derived is1to2: Powerset(Prod(D1, D2)) -> Boolean
	derived ran: Powerset(Prod(D1, D2)) -> Powerset(D2)
definitions:
	function dom($f in Powerset(Prod(D1, D2))) =
		{$d1 in D1, $d2 in D2 |
			contains($f, ($d1, $d2)): $d1}
	function isfun($f in Powerset(Prod(D1, D2))) =
		isEmpty({$d1 in D1, $d21 in D2, $d22 in D2 |
			contains($f, ($d1, $d21))
			and contains($f, ($d1, $d22))
			and neq($d21, $d22): $d21})
	function issurfun($f in Powerset(Prod(D1, D2))) =
		isfun($f) and eq(D2, {$d1 in D1, $d2 in D2 |
			contains($f, ($d1, $d2)): $d2})
	function is1to2($r in Powerset(Prod(D1, D2))) =
		eq(D1, {$d1 in dom($r), $d21 in D2, $d22 in D2 |
			contains($r, ($d1, $d21))
			and contains($r, ($d1, $d22))
			and neq($d21, $d22): $d1})
	invariant inv_f1_fun over f1: isfun(f1)%*\label{lbl:data/asmetal-inv-start}*)
	invariant inv_f2_surfun over f2: issurfun(f2)
	invariant inv_r1_1to2 over r1: is1to2(r1)%*\label{lbl:data/asmetal-inv-end}*)
\end{lstlisting}
\end{minipage}
%
\caption{Composite units of data in snapshot declarations across
  languages (part one)}
\label{fig:data/cons-mult}
\end{figure*}
% --------------------------------------------------------------------
\begin{figure*}
%
\ContinuedFloat
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=alloy]
// Alloy
sig Example {
  f1: A -> one B,%*\label{lbl:data/alloy-f1}*)
  f2: A some -> one B,%*\label{lbl:data/alloy-f2}*)
  R1: C -> B,%*\label{lbl:data/alloy-R1}*)
  s1: seq A%*\label{lbl:data/alloy-s1}*)
}

fact R1_multiplicity {%*\label{lbl:data/alloy-R1f-start}*)
  all a: A | #(a.R1) = 2
}%*\label{lbl:data/alloy-R1f-end}*)
\end{lstlisting}
\end{minipage}
%
\begin{minipage}[t]{0.49\textwidth}
\begin{lstlisting}[style=dash]
// Dash
state Example {
  f1: A -> one B,
  env f2: A some -> one B,%*\label{lbl:data/dash-env}*)
  R1: C -> B, %* \label{lbl:data/dash-R-subtype} *)
  s1: seq A,

  fact R1_multiplicity {%*\label{lbl:data/dash-fact2-start}*)
    all a: A | #(a.R1) = 2
  } %* \label{lbl:data/dash-fact2-end} *)
}
\end{lstlisting}
\end{minipage}

\begin{minipage}[t]{0.50\textwidth}
\begin{lstlisting}[style=tla]
\* TLA+
EXTENDS Integers, FiniteSets, Sequences
VARIABLES f1, f2, R1, s1

\* helper operators
Range(f) == {f[x] : x \in DOMAIN f} %*\label{lbl:data/tla-range}\label{lbl:data/tla-ops-start}*)
SurFun(a, b) == {f \in [a -> b] : b = Range(f)}
RelRange(R) == {x[2] : x \in R}
RelDomRes(S, R) == {x \in R : x[1] \in S}
OneToN(R, n) ==
  \A x \in RelDom(R) :
    Cardinality(RelRan(RelDomRes(R, {x}))) = n%*\label{lbl:data/tla-ops-end}*)

TypeOK ==
  /\ f1 \in [A -> B]%*\label{lbl:data/tla-f1}\label{lbl:data/tla-typeok-start}*)
  /\ f2 \in SurFun(A, B)%*\label{lbl:data/tla-f2}*)
  /\ R1 \in C \X B  \* \X is cross product%*\label{lbl:data/tla-R1}*)
  /\ OneToN(R1, 2)%*\label{lbl:data/tla-R1-1to2}*)
  /\ s1 \in Seq(A)%*\label{lbl:data/tla-s1}\label{lbl:data/tla-typeok-end}*)
\end{lstlisting}
\end{minipage}
\begin{minipage}[t]{0.50\textwidth}
\begin{lstlisting}[style=pluscal]
\* PlusCal
EXTENDS Integers, FiniteSets, Sequences

(* --algorithm example
variables f1, f2, R1, s1;

define
\* helper operators
Range(f) == {f[x] : x \in DOMAIN f}
\* ... all helpers identical to the TLA+ ones

TypeOK ==
  /\ f1 \in [A -> B]
  /\ f2 \in SurFun(A, B)
  /\ R1 \in C \X B  \* \X is cross product
  /\ OneToN(R1, 2)
  /\ s1 \in Seq(A)
end define
end algorithm *)
\end{lstlisting}
\end{minipage}
%
\caption{Composite units of data in snapshot declarations across
  languages (part two)}
\end{figure*}


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