% Options for packages loaded elsewhere
\PassOptionsToPackage{unicode}{hyperref}
\PassOptionsToPackage{hyphens}{url}
%
\documentclass[
]{article}
\usepackage{amsmath,amssymb}
\usepackage{iftex}
\ifPDFTeX
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
  \usepackage{textcomp} % provide euro and other symbols
\else % if luatex or xetex
  \usepackage{unicode-math} % this also loads fontspec
  \defaultfontfeatures{Scale=MatchLowercase}
  \defaultfontfeatures[\rmfamily]{Ligatures=TeX,Scale=1}
\fi
\usepackage{lmodern}
\ifPDFTeX\else
  % xetex/luatex font selection
\fi
% Use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
\IfFileExists{microtype.sty}{% use microtype if available
  \usepackage[]{microtype}
  \UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\makeatletter
\@ifundefined{KOMAClassName}{% if non-KOMA class
  \IfFileExists{parskip.sty}{%
    \usepackage{parskip}
  }{% else
    \setlength{\parindent}{0pt}
    \setlength{\parskip}{6pt plus 2pt minus 1pt}}
}{% if KOMA class
  \KOMAoptions{parskip=half}}
\makeatother
\usepackage{xcolor}
\usepackage{color}
\usepackage{fancyvrb}
\newcommand{\VerbBar}{|}
\newcommand{\VERB}{\Verb[commandchars=\\\{\}]}
\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\}}
% Add ',fontsize=\small' for more characters per line
\newenvironment{Shaded}{}{}
\newcommand{\AlertTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\AnnotationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\AttributeTok}[1]{\textcolor[rgb]{0.49,0.56,0.16}{#1}}
\newcommand{\BaseNTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\BuiltInTok}[1]{\textcolor[rgb]{0.00,0.50,0.00}{#1}}
\newcommand{\CharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\CommentTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textit{#1}}}
\newcommand{\CommentVarTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\ConstantTok}[1]{\textcolor[rgb]{0.53,0.00,0.00}{#1}}
\newcommand{\ControlFlowTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\DataTypeTok}[1]{\textcolor[rgb]{0.56,0.13,0.00}{#1}}
\newcommand{\DecValTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\DocumentationTok}[1]{\textcolor[rgb]{0.73,0.13,0.13}{\textit{#1}}}
\newcommand{\ErrorTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
\newcommand{\ExtensionTok}[1]{#1}
\newcommand{\FloatTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
\newcommand{\FunctionTok}[1]{\textcolor[rgb]{0.02,0.16,0.49}{#1}}
\newcommand{\ImportTok}[1]{\textcolor[rgb]{0.00,0.50,0.00}{\textbf{#1}}}
\newcommand{\InformationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\newcommand{\KeywordTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
\newcommand{\NormalTok}[1]{#1}
\newcommand{\OperatorTok}[1]{\textcolor[rgb]{0.40,0.40,0.40}{#1}}
\newcommand{\OtherTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{#1}}
\newcommand{\PreprocessorTok}[1]{\textcolor[rgb]{0.74,0.48,0.00}{#1}}
\newcommand{\RegionMarkerTok}[1]{#1}
\newcommand{\SpecialCharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\SpecialStringTok}[1]{\textcolor[rgb]{0.73,0.40,0.53}{#1}}
\newcommand{\StringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\VariableTok}[1]{\textcolor[rgb]{0.10,0.09,0.49}{#1}}
\newcommand{\VerbatimStringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
\newcommand{\WarningTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
\setlength{\emergencystretch}{3em} % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{-\maxdimen} % remove section numbering
\ifLuaTeX
  \usepackage{selnolig}  % disable illegal ligatures
\fi
\usepackage{bookmark}
\IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available
\urlstyle{same}
\hypersetup{
  pdftitle={MoXI --- A Model Checking Intermediate Language. (Draft)},
  pdfauthor={Cesare Tinelli},
  hidelinks,
  pdfcreator={LaTeX via pandoc}}

\title{MoXI --- A Model Checking Intermediate Language. (Draft)}
\author{Cesare Tinelli}
\date{2024-02-01}

\begin{document}
\maketitle

\begin{center}\rule{0.5\linewidth}{0.5pt}\end{center}

MoXI, which stands for Model Exchange Interlingua, is an intermediate
language meant to be a common input and output standard for model
checkers for finite- and infinite-state systems, with an initial focus
is on finite-state ones.

\subsection{General Design Philosophy}\label{general-design-philosophy}

MoXI has been designed to be general enough to be an intermediate target
language for a variety of user-facing specification languages for model
checking. At the same time, MoXI is meant to be simple enough to be
easily compilable to lower level languages or be directly supported by
model checking tools based on SAT/SMT technology.

For being an intermediate language, models expressed in MoXI are meant
to be produced and processed by tools, hence it was designed to have

\begin{itemize}
\tightlist
\item
  simple, easily (machine) parsable syntax;
\item
  a rich set of data types;
\item
  minimal syntactic sugar, at least initially;
\item
  well-understood formal semantics;
\item
  a small but comprehensive set of commands;
\item
  simple translations to lower level modeling languages such as
  \href{https://link.springer.com/chapter/10.1007/978-3-319-96145-3_32}{Btor2}.
\end{itemize}

Based on these principles, MoXI provides no direct support for many of
the features offered by current hardware modeling languages such as VHDL
and Verilog or more general purpose system modeling languages such as
SMV, TLA+, PROMELA, Simulink, SCADE, Lustre. However, it strives to
offer enough capability so that problems expressed in those languages
can be reduced to problems in MoXI.

MoXI is an extension the
\href{https://smtlib.cs.uiowa.edu/language.shtml}{SMT-LIB language} with
new commands to define and verify systems. It allows the definition of
multi-component synchronous or asynchronous reactive systems. It also
allows the specification and checking of reachability conditions (or,
indirectly state and transition invariants) and deadlocks, possibly
under fairness conditions on input values.

MoXI assumes a discrete and linear notion of time and hence has a
standard trace-based semantics.

Each system definition:

\begin{itemize}
\tightlist
\item
  defines a \emph{transition system} via the use of SMT formulas,
  imposing minimal syntactic restrictions on those formulas;
\item
  is parametrized by a \emph{state signature}, a sequence of typed
  variables;
\item
  partitions state variables into input, output and local variables;
\item
  can be expressed as the synchronous or asynchronous composition of
  other systems
\item
  is \emph{hierarchical}, i.e., may include (instances of) previously
  defined systems as subsystems;
\item
  can encode both synchronous and asynchronous system composition.
\end{itemize}

The current focus on \emph{finite-state} systems. However, the language
has been designed to support the specification of infinite-state system
as well.

\subsection{Technical Preliminaries}\label{technical-preliminaries}

The base logic of MoXI is the same as that of SMT-LIB: many-sorted
first-order logic with equality and let binders. We refer to this logic
simply as FOL. When we say \emph{formula}, with no further
qualifications, we refer to an arbitrary formula of FOL (possibly with
quantifiers and let binders).

We say that a formula is \emph{quantifier-free} if it contains no
occurrences of the quantifiers \(\forall\) and \(\exists\). We say that
it is \emph{binder-free} if it is quantifier-free and also contains no
occurrences of the let binder.

The \emph{scope} of binders and the notion of \emph{free} and
\emph{bound} (occurrences of) variables in a formula are defined as
usual.

\subsubsection{Notation}\label{notation}

If \(F\) is a formula and \(\boldsymbol{x} = (x_1, \ldots, x_n)\) a
tuple of distinct variables, we write \(F[\boldsymbol{x}]\) or
\(F[x_1, \ldots, x_n]\) to express the fact that every variable in
\(\boldsymbol{x}\) is free in \(F\) (although \(F\) may have additional
free variables). We write \(\boldsymbol{x} \circ \boldsymbol{y}\) to
denote the concatenation of tuple \(\boldsymbol{x}\) with tuple
\(\boldsymbol{y}\). When it is clear from the context, given a formula
\(F[\boldsymbol{x}]\) and a tuple
\(\boldsymbol{t} = (t_1, \ldots, t_n)\) of terms of the same type as
\(\boldsymbol{x} = (x_1, \ldots, x_n)\), we write \(F[\boldsymbol{t}]\)
or \(F[t_1, \ldots, t_n]\) to denote the formula obtained from \(F\) by
simultaneously replacing each occurrence of \(x_i\) by \(t_i\) for all
\(i=1,\ldots,n\).

A formula may contain \emph{uninterpreted} constant and function
symbols, that is, symbols with no constraints on their interpretation.
For most purposes, we treat uninterpreted constants as free variables
and treat uninterpreted function symbols as \emph{second-order} free
variables.

\subsubsection{Transition systems}\label{transition-systems}

Formally, a transition system \(S\) is a pair of predicates of the form

\[S = (
   I_S [\boldsymbol i, \boldsymbol o,  \boldsymbol s],~
   T_S [\boldsymbol i, \boldsymbol o, \boldsymbol s,
        \boldsymbol{i'}, \boldsymbol{o'}, \boldsymbol{s'}]
)\]

where

\begin{itemize}
\tightlist
\item
  \(\boldsymbol i\) and \(\boldsymbol{i'}\) are two tuples of
  \emph{input variables} with the same length and type;
\item
  \(\boldsymbol o\) and \(\boldsymbol{o'}\) are two tuples of
  \emph{output variables} with the same length and type;
\item
  \(\boldsymbol s\) and \(\boldsymbol{s'}\) are two tuples of
  \emph{local variables} with the same length and type;
\item
  \(I_S\) is the system's \emph{initial state condition}, expressed as a
  formula with no (free) variables from \(\boldsymbol{i'}\),
  \(\boldsymbol{o'}\), and \(\boldsymbol{s'}\);
\item
  \(T_S\) is the system's \emph{transition condition}, expressed as a
  formula over the variables \(\boldsymbol{i}\), \(\boldsymbol{o}\),
  \(\boldsymbol{s}\), \(\boldsymbol{i'}\), \(\boldsymbol{o'}\), and
  \(\boldsymbol{s'}\).
\end{itemize}

\begin{quote}
\textbf{Note:} For convenience, but differently from other
formalizations, a (full) state of system \(S\) is expressed by a
valuation of the variables
\(\boldsymbol{i},\boldsymbol{o},\boldsymbol{s}\). In other words, input
and output variables are automatically \emph{stateful} since the
transition relation formula can access old values of inputs and outputs
in addition to the old values of the local state. This means that,
technically, \(S\) is a closed system. The designation of some state
variables as input or output is, however, important when combining
systems together, to capture which of the state values are shared
between two systems being combined, and how.

\textbf{Note:} Similarly to Mealy machines, the initial state condition
is also meant to specify the initial system's output, based on the
initial state and input. Correspondingly, the transition relation is
also meant to specify the system's output in every later state of the
computation.

\textbf{Note:} The input and output values corresponding to the
transition to the \emph{new} state are those in the variables
\(\boldsymbol{i'}\) and \(\boldsymbol{o'}\). The values of
\(\boldsymbol{i}, \boldsymbol{o}\) are the \emph{old} input and output
values.
\end{quote}

\subsubsection{Trace Semantics}\label{trace-semantics}

A transition system in the sense above implicitly defines a model (i.e.,
a Kripke structure) of First-Order Linear Temporal Logic (FO-LTL).

The language of FO-LTL extends that of FOL with the same modal operators
of time as in standard (propositional) LTL: \(\mathbf{always},\)
\(\mathbf{eventually},\) \(\mathbf{next},\) \(\mathbf{until},\)
\(\mathbf{release}\). For our purposes of defining the semantics of
transition systems it is enough to consider just the \(\mathbf{always}\)
and \(\mathbf{eventually}\) operators.

The set of non-temporal operators depends on the particular theory, in
the sense of SMT, considered (linear integer/real arithmetic, bit
vectors, strings, and so on, and their combinations). The meaning of
theory symbols (such as arithmetic operators) and theory sorts (such as
\(\mathsf{Int}\), \(\mathsf{Real},\) \(\mathsf{Array(Int, Real)},\)
\(\mathsf{BitVec(3)}\), \(\ldots\)) is fixed by the theory
\(\mathcal T\) in question. Once a theory \(\mathcal T\) has been fixed
then, the meaning of a FO-LTL formula \(F\) is provided by an
interpretation of the uninterpreted (constant and function) symbols of
\(F\), if any, as well as an infinite sequence of valuations for the
free variables of \(F\).

More precisely, let us fix a tuple \(\boldsymbol x = (x_1,\ldots,x_n)\)
of distinct \emph{state} variables, meant to represent the state of a
computation system. We will denote by \(\boldsymbol{x'}\) the tuple
\((x_1',\ldots,x_n')\) and write formulas of the form
\(F[\boldsymbol f, \boldsymbol x, \boldsymbol x']\) where
\(\boldsymbol f\) is a tuple of uninterpreted symbols. If \(F\) has free
occurrences of variables from \(\boldsymbol x\) but not from
\(\boldsymbol{x'}\) we call it a \emph{one-state} formula; otherwise, we
call it a \emph{two-state} formula.

A \emph{valuation of} \(\boldsymbol x\), or a \emph{state over}
\(\boldsymbol x\), is function mapping each variable \(x\) in
\(\boldsymbol x\) to a value of \(x\)'s type. Let \(\kappa\) be a
positive ordinal smaller than \(\omega\), the cardinality of the natural
numbers. A \emph{trace (of length} \(\kappa\)\emph{)} is any state
sequence \(\pi = (s_j  \mid 0 \leq j < \kappa)\). Note that \(\pi\) is
the finite sequence \(s_0, \ldots, s_{\kappa-1}\) when
\(\kappa < \omega\) and is the infinite sequence \(s_0, s_1, \ldots\)
otherwise. For all \(i\) with \(0 \leq i < \kappa\) , we denote by
\(\pi[i]\) the state \(s_i\) and by \(\pi^i\) the subsequence
\((s_j \mid i \leq j < \kappa)\).

\subsubsection{Infinite-Trace Semantics}\label{infinite-trace-semantics}

Let \(F[\boldsymbol f, \boldsymbol x, \boldsymbol{x'}]\) be a formula as
above. If \(\mathcal I\) is an interpretation of \(\boldsymbol{f}\) in
the theory \(\mathcal T\) and \(\pi\) is an infinite trace, then
\((\mathcal I, \pi)\) \emph{satisfies} \(F\), written
\((\mathcal I, \pi) \models F\), iff

\begin{itemize}
\tightlist
\item
  \(F\) is atomic and
  \(\mathcal{I}[\boldsymbol x \mapsto \pi[0](\boldsymbol x),\boldsymbol{x'} \mapsto \pi[1](\boldsymbol x)]\)
  satisfies \(F\) as in FOL;
\item
  \(F = \lnot G~\) and \(~(\mathcal I, \pi) \not\models G\);
\item
  \(F = G_1 \land G_2~\) and \(~(\mathcal I, \pi) \models G_i\) for
  \(i=1,2\);
\item
  \(F = \exists x\, G\) and \((\mathcal I[z \mapsto v], \pi) \models G\)
  for some value \(v\) for \(x\);
\item
  \(F = \mathbf{eventually}~G\) and \((\mathcal I, \pi^i) \models G\)
  for some \(i \geq 0\);
\item
  \(F = \mathbf{always}~G\) and \((\mathcal I, \pi^i) \models G\) for
  all \(i \geq 0\).
\end{itemize}

The semantics of the propositional connectives
\(\lor, \rightarrow, \leftrightarrow\) and the quantifier \(\forall\)
can be defined by reduction to the connectives above (e.g., by defining
\(G_1 \lor G_2\) as \(\lnot(\lnot G_1 \land \lnot G_2)\) and so on).
Note that \(\exists\) is a \emph{static}, or \emph{rigid}, quantifier:
the meaning of the variable it quantifies does not change over time,
that is, from state to state in \(\pi\). The same is true for
uninterpreted symbols. They are \emph{rigid} in the same sense: their
meaning does not change over time. Another way to understand the
difference between rigid and non-rigid symbols is that state variables
are mutable over time whereas quantified variables, theory symbols and
uninterpreted symbols are all immutable.

Now let

\[S = (I_S [\boldsymbol i, \boldsymbol o,  \boldsymbol s],~
       T_S [\boldsymbol i, \boldsymbol o, \boldsymbol s, \boldsymbol{i'}, \boldsymbol{o'}, \boldsymbol{s'}]
)\]

be a transition system with state variables
\(\boldsymbol i, \boldsymbol o,  \boldsymbol s\).

The \emph{infinite trace semantics} of \(S\) is the set of all pairs
\((\mathcal I, \pi)\) of interpretations \(\mathcal I\) in
\(\mathcal T\) and infinite traces \(\pi\) such that

\[(\mathcal I, \pi) \models
  I_S \land\ \mathbf{always}~T_S
\]

We call any such pair an \emph{execution} of \(S\).

\begin{quote}
\textbf{Note:} {[}We focus on reactive systems{]}
\end{quote}

\subsubsection{Finite-Trace Semantics}\label{finite-trace-semantics}

Let \(F[\boldsymbol f, \boldsymbol x, \boldsymbol{x'}]\),
\(\mathcal I\), \(\mathcal T\) and \(\pi\) be defined is in the
subsection above. For every \(n \geq 0\), \((\mathcal I, \pi)\)
\(n\)\emph{-satisfies} \(F\), written \((\mathcal I, \pi) \models_n F\),
iff

\begin{itemize}
\item
  \(F\) is atomic and
  \(\mathcal I[\boldsymbol x \mapsto \pi[0](\boldsymbol x), \boldsymbol{x'} \mapsto \pi[1](\boldsymbol x)]\)
  satisfies \(F\) as in FOL;
\item
  \(F = \lnot G\) and \((\mathcal I, \pi) \not\models_n G\)
\item
  \(F = G_1 \land G_2\) and \((\mathcal I, \pi) \models_n G_i\) for
  \(i=1,2\);
\item
  \(F = \exists x\, G\) and
  \((\mathcal I[z \mapsto v], \pi) \models_n G\) for some value \(v\)
  for \(x\);
\item
  \(F = \mathbf{eventually}~G\) and
  \((\mathcal I, \pi^i) \models_{n-i} G\) for some \(i = 0, \ldots, n\);
\item
  \(F = \mathbf{always}~G\) and \((\mathcal I, \pi^i) \models_{n-i} G\)
  for all \(i = 0, \ldots, n\);
\end{itemize}

The semantics of the propositional connectives
\(\lor, \rightarrow, \leftrightarrow\) and the quantifier \(\forall\) is
again defined by reduction to the connectives above.

Intuitively, \(n\)-satisfiability specifies when a formula is true over
the first \(n\) states of a trace. Note that this notion is well defined
even when \(n=0\) regardless of whether \(F\) has free occurrences of
variables from \(\boldsymbol{x'}\) or not. In the atomic case, this is
true because \(\pi\), for being an \emph{infinite} trace, does contain
the state \(\pi[1]\). In the general case, the claim can be shown by a
simple inductive argument.

The notion of \(n\)-satisfiability is useful when one is interested, as
we are, in state reachability. The reason is that a state satisfying a
(non-temporal) state property \(R\) is reachable in a system \(S\) only
if the temporal formula \(\mathbf{eventually}~R\) is \(n\)-satisfied by
an execution of \(S\) for some \(n\). Note, however, that the converse
does not hold. That is, it is possible for \(R\) to be reachable in a
system \(S\) without being \(n\)-satisfied by an execution of \(S\). See
Section \hyperref[add_link]{todo} for more details.

\subsection{Supported SMT-LIB
commands}\label{supported-smt-lib-commands}

SMT-LIB is a command-based language with LISP-like syntax
(\href{https://en.wikipedia.org/wiki/S-expression}{s-expressions}, in
prefix notation) designed to be a common input/output language for SMT
solvers.

MoXI adopts the following SMT-LIB commands:

\begin{itemize}
\item
  (declare-sort \(s\) \(n\))

  Declares \(s\) to be a sort symbol (i.e., type constructor) of arity
  \(n\). Examples:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(declare{-}sort A 0)}
\NormalTok{(declare{-}sort Set 1)}
\NormalTok{; possible sorts: A, (Set A), (Set (Set A)), (Array Int Real), ...}
\end{Highlighting}
\end{Shaded}
\item
  (define-sort \(s\) ( \(u_1\) \(\cdots\) \(u_n\) ) \(\tau\))

  Defines \(S\) as synonym of a parametric type \(\tau\) with parameters
  \(u_1 \cdots u_n\). Examples:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(declare{-}sort NestedSet (X) (Set (Set X)))}
\NormalTok{; possible sorts: (NestedSet A), ...}
\NormalTok{(declare{-}sort Array2 (X Y) (Array X (Array X Y)))}
\NormalTok{; possible sorts: (Array2 Int Bool), ...}
\end{Highlighting}
\end{Shaded}
\item
  (declare-const \(c\) \(\sigma\))

  Declares a constant \(c\) of sort \(\sigma\). Examples:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(declare{-}const a A)}
\NormalTok{(declare{-}const n Int)}
\end{Highlighting}
\end{Shaded}
\item
  (define-fun \(f\) ( ( \(x_1\) \(\sigma_1\) ) \(\cdots\) ( \(x_1\)
  \(\sigma_1\) ) ) \(\sigma\) \(t\))

  Defines a (non-recursive) function \(f\) with inputs
  \(x_1, \ldots, x_n\) (of respective sort
  \(\sigma_1, \ldots, \sigma_n\)), output sort \(\sigma\), and body
  \(t\). Examples:

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(declare{-}fun sq ((n Int)) Int (* n n))}
\NormalTok{(declare{-}fun isSqRoot ((m Int) (n Int)) Bool (= n (sq m)))}
\NormalTok{(declare{-}fun max ((m Int) (n Int)) Int (ite (\textgreater{} m n) m n))}
\end{Highlighting}
\end{Shaded}
\item
  (set-logic \(L\))

  Defines the model's \emph{data logic}, that is, the background
  theories of relevant data types (e.g., integers, reals, bit vectors,
  and so on) as well as the language of allowed logical constraints
  (e.g., quantifier-free, linear, etc.).

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(set{-}logic QF\_BV)}
\end{Highlighting}
\end{Shaded}
\end{itemize}

One addition to SMT-LIB is the binary symbol != for disequality. For
each term s and t of the same sort, (!= s t) has the same meaning as
(not (= s t)) or, equivalently, (distinct s t).

\subsection{MoXI-specific commands}\label{moxi-specific-commands}

\subsubsection{Enumeration declaration}\label{enumeration-declaration}

(declare-enum-sort \(s\) ( \(c_1\) \(\cdots\) \(c_n\) ) )

Declares \(s\) to be an enumerative type with (distinct) values
\(c_1, \ldots, c_n\).

\subsubsection{System definition
command}\label{system-definition-command}

\paragraph{Atomic systems}\label{atomic-systems}

An atomic transition system is defined by a command of the form:

(define-system \(S\) ~:input ( ( \(i_1\) \(\delta_1\) ) \(\cdots\) (
\(i_m\) \(\delta_m\)) ) ~:output ( ( \(o_1\) \(\tau_1\) ) \(\cdots\) (
\(o_n\) \(\tau_n\) ) ) ~:local ( ( \(s_1\) \(\sigma_1\) ) \(\cdots\) (
\(s_p\) \(\sigma_p\) ) ) ~:init \(I\) ~:trans \(T\) ~:inv \(P\) )

where

\begin{itemize}
\tightlist
\item
  \(S\) is the system's identifier;
\item
  each \(i_j\) is an \emph{input} variable of sort \(\delta_j\);
\item
  each \(o_j\) is an \emph{output} variable of sort \(\tau_j\);
\item
  each \(s_j\) is a \emph{local} variable of sort \(\sigma_j\);
\item
  all variables abo
\item
  each \(i_j\), \(o_j\), \(s_j\) denote \emph{current-state} values
\item
  \emph{next-state variables} are not provided explicitly but are
  denoted by convention by appending \('\) to the names of the
  current-state variables \(i_j\), \(o_j\), and \(s_j\);
\item
  \(I\), \emph{the initial condition}, is a one-state formula over the
  unprimed system's variables (input, output and local state variables)
  that expresses a constraint on the initial states of \(S\);
\item
  \(T\), \emph{the transition condition,} is a two-state formula over
  all of the system's variables (primed and unprimed) that expresses a
  constraint on the state transitions of \(S\);
\item
  \(P\), \emph{the invariance condition}, is a one state formula over
  all of the \emph{unprimed} system's variables that expresses a
  constraint on all reachable states of \(S\);
\item
  all attributes are optional but can occur at most once;
\item
  the order of the attributes is immaterial except that :input, :output,
  and :local must occur before :init, :trans, and :inv;
\item
  the default value for a missing attribute is the empty list () for
  :input, :output, and :local; and true for :init, :trans, and :inv.
\end{itemize}

Syntactically, the system identifier, the input, output and local
variables are SMT-LIB symbols. In contrast, the sorts \(\delta_j\),
\(\tau_j\), \(\sigma_j\) are SMT-LIB sorts, while the formulas \(I\),
\(T\) and \(P\) are SMT-LIB terms of type Bool.

\begin{quote}
\textbf{Discussion:} We could allow multiple occurrences of the :inv
attribute with conjunctive semantics. Should we allow multiple
occurrences of the :trans attribute but with \emph{disjunctive}
semantics? The rationale would be to facilitate the recognition of
systems defined by alternative sets of transitions.
\end{quote}

\paragraph{Atomic System Semantics}\label{atomic-system-semantics}

Let \(\boldsymbol{i} = (i_1, \ldots, i_m)\),
\(\boldsymbol{o} = (o_1, \ldots, o_n)\),
\(\boldsymbol{s} = (s_1, \ldots, s_p)\), and \(\boldsymbol{v}\) =
\(\boldsymbol{i},\boldsymbol{o},\boldsymbol{s}\).

Formally, an atomic system \(S\) introduced by the define-system command
above is a transition system whose behavior consists of all the
(infinite) executions \((\mathcal I, \pi)\) over \(\boldsymbol{v}\) such
that

\[(\mathcal I, \pi) \models
  I[\boldsymbol{v}] \land \mathbf{always}\ (P[\boldsymbol{v}] \land T[\boldsymbol{v},\boldsymbol{v'}]) \ .
\]

We call \(I_S = I[\boldsymbol{v}]\) \emph{the initial state predicate}
of \(S\) and
\(T_S = P[\boldsymbol{v}] \land T[\boldsymbol{v},\boldsymbol{v'}]\)
\emph{the transition predicate} of \(S\).

\begin{quote}
\textbf{Note:} The relation expressed by the formula \(T\) is not
required to be functional over
\(\boldsymbol{i},\boldsymbol{o},\boldsymbol{s},\boldsymbol{i'}\), thus
allowing the modeling of non-deterministic systems.

\textbf{Note:} The :inv attribute is not strictly necessary since a
system with a declaration of the form

(define-system \(S\) :input ( ( \(i_1\) \(\sigma_1\) ) \(\cdots\) (
\(i_m\) \(\sigma_m\) ) ) ~:output ( ( \(o_1\) \(\tau_1\) ) \(\cdots\) (
\(o_n\) \(\tau_n\) ) ) ~:local ( ( \(s_1\) \(\sigma_1\) ) \(\cdots\) (
\(s_p\) \(\sigma_p\) ) ) ~:init \(I\) ~:trans \(T\) ~:inv \(P\) )

can be equivalently expressed with a declaration of the form

(define-system \(S\) :input ( ( \(i_1\) \(\sigma_1\) ) \(\cdots\) (
\(i_m\) \(\sigma_m\) ) ) ~:output ( ( \(o_1\) \(\tau_1\) ) \(\cdots\) (
\(o_n\) \(\tau_n\) ) ) ~:local ( ( \(s_1\) \(\sigma_1\) ) \(\cdots\) (
\(s_p\) \(\sigma_p\) ) ) ~:init \(I\) ~:trans (and \(P\) \(T\)) )
\end{quote}

\begin{quote}
\textbf{Note:} Systems are meant to be progressive: every reachable
state has a successor with respect \(T_S\). However, they may not be
because of the generality of \(T\) and \(P\). In other words, it is
possible to define deadlocking systems. (See later for more details on
deadlocked states.)
\end{quote}

\paragraph{Examples}\label{examples}

(Adapted from ``Principles of Cyber-Physical Systems'' by R. Alur, 2015)

When reading these examples, it is helpful to keep in mind that,
intuitively, in the :init formulas the input values are given and the
local and output values are to be defined with respect to them. In
contrast, in the :trans formulas the new input values, and old input,
output and local values are given, and the new local and output values
are to be defined.

The output of system Delay below is initially 0 and then is the previous
input. No local variables are needed.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system Delay :input ( (i Int) ) :output ( (o Int) )}
\NormalTok{ :init (= o 0)}
\NormalTok{ :trans (= o\textquotesingle{} i) ; the new output is the old input}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

A variant of Delay where the output is initially any number in
{[}0,10{]}.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system Delay :input ( (i Int) ) :output ( (o Int) )}
\NormalTok{ :init (\textless{}= 0 o 10) ; more than one possible initial output}
\NormalTok{ :trans (= o\textquotesingle{} i)}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

A clocked lossless channel, stuttering when the clock is not ticking.
The clock is represented by a Boolean input variable clock.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system StutteringClockedCopy}
\NormalTok{ :input ((clock Bool) (i Int))}
\NormalTok{ :output ((o Int))}
\NormalTok{ :init (=\textgreater{} clock (= o i)) ; o is arbitrary when clock is false }
\NormalTok{ :trans (ite clock (= o’ i’) (= o’ o)) ; ite is if{-}then{-}else}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

Events carrying data can be modeled as instances of the polymorphic
algebraic datatype (Event X) where X is the type of the data carried by
the event.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(declare{-}datatype Event (par (X) (}
\NormalTok{  (absent)}
\NormalTok{  (present (val X))}
\NormalTok{)))}
\end{Highlighting}
\end{Shaded}

An event-triggered channel that arbitrarily loses its input data.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system LossyIntChannel}
\NormalTok{ :input ((i (Event Int)))}
\NormalTok{ :output ((o (Event Int)))}
\NormalTok{ :inv (or (= o i) (= o absent))}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

Equivalent formulation using unconstrained local state.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system LossyIntChannel}
\NormalTok{ :input ((i (Event Int))) }
\NormalTok{ :output ((o (Event Int)))}
\NormalTok{ :local ((s Bool))}
\NormalTok{ ; at all times, whether the input event is transmitted }
\NormalTok{ ; or not depends on value of s}
\NormalTok{ :inv (= o (ite s i absent))}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

TimedSwitch models a timed light switch where the light stays on for at
most 10 steps unless it is switched off before. The input Boolean is
interpreted as an on/off toggle. The transition predicate is formulated
as a set of transitions.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(declare{-}enum{-}sort LightStatus (on off))}

\NormalTok{(define{-}system TimedSwitch1}
\NormalTok{ :input ( (press Bool) )}
\NormalTok{ :output ( (sig Bool) )}
\NormalTok{ :local ( (s LightStatus) (n Int) )}
\NormalTok{ :inv (= sig (= s on))}
\NormalTok{ :init (and}
\NormalTok{   (= n 0)}
\NormalTok{   (ite press (= s on) (= s off))}
\NormalTok{ )}
\NormalTok{ :trans (let}
\NormalTok{  (; transitions}
\NormalTok{   (stay{-}off (and (= s off) (not press\textquotesingle{}) (= s\textquotesingle{} off) (= n\textquotesingle{} n)))}
\NormalTok{   (turn{-}on  (and (= s off) press\textquotesingle{} (= s\textquotesingle{} on) (= n\textquotesingle{} n)))}
\NormalTok{   (stay{-}on  (and (= s on) (not press\textquotesingle{}) (\textless{} n 10) (= s\textquotesingle{} on) (= n\textquotesingle{} (+ n 1))))}
\NormalTok{   (turn{-}off (and (= s on) (or press\textquotesingle{} (\textgreater{}= n 10)) (= s\textquotesingle{} off) (= n\textquotesingle{} 0)))}
\NormalTok{  )}
\NormalTok{  (or stay{-}off turn{-}on turn{-}off stay{-}on)}
\NormalTok{ )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

A variant of the system above where the transition predicate is
formulated guarded-transitions style.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system TimedSwitch2}
\NormalTok{ :input ( (press Bool) )}
\NormalTok{ :output ( (sig Bool) )}
\NormalTok{ :local ( (s LightStatus) (n Int) )}
\NormalTok{ :inv (= sig (= s on))}
\NormalTok{ :init (and}
\NormalTok{    (= n 0)}
\NormalTok{    (ite press (= s on) (= s off))}
\NormalTok{  )}
\NormalTok{ :trans (and}
\NormalTok{   (=\textgreater{} (and (= s off) (not press\textquotesingle{}))}
\NormalTok{       (and (= s\textquotesingle{} off) (= n\textquotesingle{} n)))            ; off {-}{-}\textgreater{} off}
\NormalTok{   (=\textgreater{} (and (= s off) press\textquotesingle{})}
\NormalTok{       (and (= s\textquotesingle{} on) (= n\textquotesingle{} n)))             ; off {-}{-}\textgreater{} on}
\NormalTok{   (=\textgreater{} (and (= s on) (not press\textquotesingle{}) (\textless{} 10 n))}
\NormalTok{        (and (= s\textquotesingle{} on) (= n\textquotesingle{} (+ n 1))))      ; on {-}{-}\textgreater{} on}
\NormalTok{   (=\textgreater{} (and (= s on) (or press\textquotesingle{} (\textgreater{}= n 10)))}
\NormalTok{       (and (= s\textquotesingle{} off) (= n\textquotesingle{} 0)))            ; on {-}{-}\textgreater{} off}
\NormalTok{  )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

Another variant but in equational style.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}fun flip ((s LightStatus)) LightStatus}
\NormalTok{  (ite (= s off) on off)}
\NormalTok{)}

\NormalTok{(define{-}system TimedSwitch3}
\NormalTok{ :input ( (press Bool) )}
\NormalTok{ :output ( (sig Bool) )}
\NormalTok{ :local ( (s LightStatus) (n Int) )}
\NormalTok{ :inv (= sig (= s on))}
\NormalTok{ :init (and}
\NormalTok{   (= n 0)}
\NormalTok{   (= s (ite press on off))}
\NormalTok{ )}
\NormalTok{ :trans (and}
\NormalTok{   (= s\textquotesingle{} (ite press\textquotesingle{} (flip s)}
\NormalTok{            (ite (or (= s off) (\textgreater{}= n 10)) off}
\NormalTok{              on)))}
\NormalTok{   (= n\textquotesingle{} (ite (or (= s off) (= s\textquotesingle{} off)) 0}
\NormalTok{            (+ n 1)))}
\NormalTok{  )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

The non-deterministic arbiter below grants input requests expressed by
the Boolean inputs r1 and r2. A request is always granted, expressed by
the Boolean outputs g1 or grant2, if it is the only request. When both
inputs contain a request, one of the two request is granted, with a
non-deterministic choice. Since the output depends only on the current
values of input and local variables, the systems can be specified simply
by an invariant.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system NonDetArbiter}
\NormalTok{ :input ( (r1 Bool) (r2 Bool) )}
\NormalTok{ :output ( (g1 Bool) (g2 Bool) )}
\NormalTok{ :local ( (s Bool) )}
\NormalTok{ :inv (and}
\NormalTok{  (=\textgreater{} (and (not r1) (not r2))}
\NormalTok{      (and (not g1) (not g2)))}
\NormalTok{  (=\textgreater{} (and r1 (not r2))}
\NormalTok{      (and g1 (not g2)))}
\NormalTok{  (=\textgreater{} (and (not r1) r2)}
\NormalTok{      (and (not g1) g2))}
\NormalTok{  (=\textgreater{} (and r1 r2)}
\NormalTok{      ; the unconstrained value of \textasciigrave{}s\textasciigrave{} is used as non{-}deterministic choice}
\NormalTok{      (ite s (and g1 (not g2))}
\NormalTok{        (and (not g1) g2)))}
\NormalTok{  )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

The next arbiter is similar to NonDetArbiter but grants requests a cycle
later and does not use a local variable for the non-deterministic
choice.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system DelayedArbiter}
\NormalTok{ :input ( (r1 Bool) (r2 Bool) )}
\NormalTok{ :output ( (g1 Bool) (g2 Bool) )}
\NormalTok{ :local ( (s Bool) )}
\NormalTok{ :init ( and (not g1) (not g2) )  ; nothing is granted initially}
\NormalTok{ :trans (and}
\NormalTok{    (=\textgreater{} (and (not r1) (not r2))}
\NormalTok{        (and (not g1\textquotesingle{}) (not g2\textquotesingle{})))}
\NormalTok{    (=\textgreater{} (and r1 (not r2))}
\NormalTok{        (and g1\textquotesingle{} (not g2\textquotesingle{})))}
\NormalTok{    (=\textgreater{} (and (not r1) r2)}
\NormalTok{        (and (not g1\textquotesingle{}) g2\textquotesingle{}))}
\NormalTok{    (=\textgreater{} (and r1 r2)}
\NormalTok{        (!= g1\textquotesingle{} g2\textquotesingle{}))}
\NormalTok{  )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

Similar to DelayedArbiter but for requests expressed as integer events.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system IntNonDetArbiter}
\NormalTok{  :input ( (r1 (Event Int)) (r2 (Event Int)) )}
\NormalTok{  :output ( (g1 (Event Int)) (g2 (Event Int)) )}
\NormalTok{  :local ( (s Bool) )}
\NormalTok{  :init (= g1 g2 absent)}
\NormalTok{  :trans (and}
\NormalTok{    (=\textgreater{} (= r1\textquotesingle{} r2\textquotesingle{} absent)}
\NormalTok{        (= g1\textquotesingle{} g2\textquotesingle{} absent))}
\NormalTok{    (=\textgreater{} (and (!= r1\textquotesingle{} absent) (= r2\textquotesingle{} absent))}
\NormalTok{        (and (= g1\textquotesingle{} r1) (= g2\textquotesingle{} absent)))}
\NormalTok{    (=\textgreater{} (and (= r1\textquotesingle{} absent) (!= r2\textquotesingle{} absent))}
\NormalTok{        (and (= g1\textquotesingle{} absent) (= g2\textquotesingle{} r2\textquotesingle{})))}
\NormalTok{    (=\textgreater{} (and (!= r1\textquotesingle{} absent) (!= r2\textquotesingle{} absent))}
\NormalTok{        (or (and (= g1\textquotesingle{} r1\textquotesingle{}) (= g2\textquotesingle{} absent))}
\NormalTok{          (and (= g1\textquotesingle{} absent) (= g2\textquotesingle{} r2\textquotesingle{}))))}
\NormalTok{  )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

\paragraph{Composite Systems - synchronous
composition}\label{composite-systems---synchronous-composition}

A transition systems can be defined as the synchronous composition of
other systems by a command of the form:

(define-system \(S\) ~:input ( ( \(i_1\) \(\sigma_1\) ) \(\cdots\) (
\(i_m\) \(\sigma_m\) ) ) ~:output ( ( \(o_1\) \(\tau_1\) ) \(\cdots\) (
\(o_n\) \(\tau_n\) ) ) ~:local ( ( \(s_1\) \(\sigma_1\) ) \(\cdots\) (
\(s_p\) \(\sigma_p\) ) ) ~:subsys ( \(N_1\) ( \(S_1\)
\(\boldsymbol x_1\) \(\boldsymbol y_1\) ) ) ~~ \(\cdots\) ~:subsys (
\(N_q\) ( \(S_q\) \(\boldsymbol x_q\) \(\boldsymbol y_q\) ) ) ~:init
\(I\) ~:trans \(T\) ~:inv \(P\) )

where

\begin{itemize}
\tightlist
\item
  :input, :output, :local :init, :trans, and :inv are as in atomic
  system definitions;
\item
  \(q > 0\) and each \(S_i\) is the name of a system other than \(S\);
\item
  the names \(S_1 \ldots,S_q\) need not be all distinct;
\item
  each \(N_i\) is a local synonym for \(S_i\), with \(N_1,\ldots,N_q\)
  distinct;
\item
  each \(\boldsymbol x_i\) consists of \(S\)'s variables of the same
  type as \(S_i\)'s input;
\item
  each \(\boldsymbol y_i\) consists of \(S\)'s local/output variables of
  the same type as \(S_i\)' '\,'s output;
\item
  the directed subsystem graph rooted at \(S\) is acyclic.
\end{itemize}

\paragraph{Composite System Semantics}\label{composite-system-semantics}

For \(k=1,\ldots, q\), let
\(S_k = (I_k[\boldsymbol{i}_k,\boldsymbol{o}_k,\boldsymbol{s}_k], T_k[\boldsymbol{i}_k,\boldsymbol{o}_k,\boldsymbol{s}_k,\boldsymbol{i'}_k,\boldsymbol{o'}_k,\boldsymbol{s'}_k])\),
with the elements of \(\boldsymbol{s}_1,\ldots, \boldsymbol{s}_q\) all
mutually distinct.

Let \(\boldsymbol{i} = (i_1, \ldots, i_m)\),
\(\boldsymbol{o} = (o_1, \ldots, o_n)\),
\(\boldsymbol{s} = (s_1, \ldots, s_p) \circ \boldsymbol{s}_1 \circ \cdots \circ \boldsymbol{s}_q\),
and \(\boldsymbol{v}\) =
\(\boldsymbol{i} \circ \boldsymbol{o} \circ \boldsymbol{s}\).

Formally, a composite system \(S\) introduced by the define-system
command above is a transition system whose behavior consists of all the
(infinite) executions \((\mathcal I, \pi)\) over \(\boldsymbol{v}\) such
that

\[(\mathcal I, \pi) \models
  I_S[\boldsymbol{v}] \land \mathbf{always}\ T_S[\boldsymbol{v},\boldsymbol{v'}]
\]

where

\begin{itemize}
\tightlist
\item
  \(I_S[\boldsymbol{v}] = I[\boldsymbol{v}] \land \bigwedge_{k=1,\ldots,q} I_k[\boldsymbol{x}_k,\boldsymbol{y}_k,\boldsymbol{s}_k]\)
  and
\item
  \(T_S[\boldsymbol{v},\boldsymbol{v'}] = P[\boldsymbol{v}] \land T[\boldsymbol{v},\boldsymbol{v'}] \land \bigwedge_{k=1,\ldots,q} T_k[\boldsymbol{x}_k,\boldsymbol{y}_k,\boldsymbol{s}_k, \boldsymbol{x'}_k,\boldsymbol{y'}_k,\boldsymbol{s'}_k]\)
\end{itemize}

\paragraph{Examples, composite
systems}\label{examples-composite-systems}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{;{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}}
\NormalTok{; Two{-}step delay}
\NormalTok{;{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}}

\NormalTok{;     +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+}
\NormalTok{;     |   DoubleDelay                      |}
\NormalTok{;     |  +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+      +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+  |}
\NormalTok{;  in |  |           | temp |           |  | out}
\NormalTok{; {-}{-}{-}{-}+{-}\textgreater{}|   Delay   |{-}{-}{-}{-}{-}\textgreater{}|   Delay   |{-}{-}+{-}{-}{-}{-}\textgreater{}}
\NormalTok{;     |  |           |      |           |  |}
\NormalTok{;     |  +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+      +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+  |}
\NormalTok{;     +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+}

\NormalTok{; One{-}step delay}
\NormalTok{(define{-}system Delay :input ( (i Int) ) :output ( (o Int) )}
\NormalTok{  :local ( (s Int) )}
\NormalTok{  :inv (= s i) }
\NormalTok{  :init (= o 0)}
\NormalTok{  :trans (= o\textquotesingle{} s)}
\NormalTok{)}

\NormalTok{; Two{-}step delay}
\NormalTok{(define{-}system DoubleDelay :input ( (in Int) ) :output ( (out Int) )}
\NormalTok{  :local ( (temp Int) )}
\NormalTok{  :subsys  (D1 (Delay in temp))}
\NormalTok{  :subsys  (D2 (Delay temp out))}
\NormalTok{)}

\NormalTok{;; DoubleDelay expanded}
\NormalTok{(define{-}system DoubleDelay}
\NormalTok{  :input ( (in Int) )}
\NormalTok{  :output ( (out Int) )}
\NormalTok{  :local ( }
\NormalTok{    (temp Int)  }
\NormalTok{    (s1 Int)      ; from \textasciigrave{}(Delay in temp)\textasciigrave{}}
\NormalTok{    (s2 Int)      ; from \textasciigrave{}(Delay temp out)\textasciigrave{}}
\NormalTok{  )}
\NormalTok{  :inv (and}
\NormalTok{    (= s1 in)     ; from \textasciigrave{}(Delay in temp)\textasciigrave{}}
\NormalTok{    (= s2 temp)   ; from \textasciigrave{}(Delay temp out)\textasciigrave{}}
\NormalTok{  )}
\NormalTok{  :init (and}
\NormalTok{    (= temp 0)   ; from \textasciigrave{}(Delay in temp)\textasciigrave{}}
\NormalTok{    (= out 0)    ; from  \textasciigrave{}(Delay temp out)\textasciigrave{}}
\NormalTok{  )}
\NormalTok{  :trans (and}
\NormalTok{    (= temp\textquotesingle{} s1) ; from \textasciigrave{}(Delay in temp)\textasciigrave{}}
\NormalTok{    (= out\textquotesingle{} s2)  ; from \textasciigrave{}(Delay temp out)\textasciigrave{}}
\NormalTok{  )}
\NormalTok{)}
\NormalTok{; Example trace:}
\NormalTok{;   in = 1, 2, 3, 4, 5, 6, 7, ...}
\NormalTok{;   s1 = 1, 2, 3, 4, 5, 6, 7, ...}
\NormalTok{; temp = 0, 1, 2, 3, 4, 5, 6, ...}
\NormalTok{;   s2 = 0, 1, 2, 3, 4, 5, 6, ...}
\NormalTok{;  out = 0, 0, 1, 2, 3, 4, 5, ...}
\end{Highlighting}
\end{Shaded}

The next example defines a three-bit counter in terms of three identical
one-bit counters. The one-bit counter uses a latch. The latch has a
Boolean state represented by state variable s with arbitrary initial
value. The value of output out is always the previous value of s. A set
request (represented by input set being true) sets the new value of s to
true unless there is a concurrent reset request (represented by input
reset being true). In that case, the choice between the two requests is
resolved arbitrarily using the value of the unconstrained local variable
b. In the absence of either a set or a reset, the value of out is
unchanged.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system Latch  :input ( (set Bool) (reset Bool) )  :output ( (out Bool)) }
\NormalTok{ :local ( (s Bool) (b Bool) )}
\NormalTok{ :init (and}
\NormalTok{   (= out b)}
\NormalTok{ )}
\NormalTok{ :trans (and}
\NormalTok{   (= out\textquotesingle{} s)}
\NormalTok{   (= s\textquotesingle{} (or (and set (or (not reset) b)) }
\NormalTok{             (and (not set) (not reset) out)))}
\NormalTok{ )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

The one-bit counter is implemented using the latch component modeled by
\texttt{Latch}. The counter goes from 0 (represented as false) to 1
(true) with a carry value of 0, or from 1 to 0 with a carry value of 1
when the increment signal inc is true. It is reset to 0 (false) when the
start signal is true. The initial value of the counter is arbitrary.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{;        +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+}
\NormalTok{;        |                                                              |}
\NormalTok{;        |   +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+ |}
\NormalTok{;        |   |                                              +{-}{-}{-}{-}{-}{-}{-}+ | |}
\NormalTok{;        | +{-}|{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}|\textasciigrave{}\textasciigrave{}{-}.  set |       | | |}
\NormalTok{;        | | |                          |\textasciigrave{}{-}.\_    |    :{-}{-}{-}{-}\textgreater{}|       | | |}
\NormalTok{;        | | +{-}{-}|\textasciigrave{}\textasciigrave{}{-}.                +{-}{-}|   \_]o{-}{-}|..{-}\textasciigrave{}      | Latch | | |}
\NormalTok{;        | |    |    :{-}{-}+{-}{-}{-}{-}\textbackslash{}\textasciigrave{}\textasciigrave{}{-}.   |  |.{-}\textasciigrave{}          reset |       |{-}+{-}{-}{-}{-}\textgreater{} out}
\NormalTok{;   inc {-}{-}{-}+{-}{-}{-}{-}|..{-}\textasciigrave{}   |     )   :{-}{-}+{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}\textgreater{}|       |   |}
\NormalTok{;        |              | +{-}{-}/..{-}\textasciigrave{}                          +{-}{-}{-}{-}{-}{-}{-}+   |}
\NormalTok{;        |              | |                                             |}
\NormalTok{; start {-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+                OneBitCounter                |}
\NormalTok{;        |              |                                               |}
\NormalTok{;        +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}|{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+}
\NormalTok{;                       |    }
\NormalTok{;                       v carry}

\NormalTok{(define{-}system OneBitCounter :input ( (inc Bool) (start Bool) ) }
\NormalTok{ :output ( (out Bool) (carry Bool) )}
\NormalTok{ :local ( (set Bool) (reset Bool) )}
\NormalTok{ :subsys (L (Latch set reset out))}
\NormalTok{ :inv (and }
\NormalTok{   (= set (and inc (not reset)))}
\NormalTok{   (= reset (or carry start))}
\NormalTok{   (= carry (and inc out))}
\NormalTok{ )}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

The three-bit counter is a resettable counter obtained by cascading
three 1-bit counters. The output is three Boolean values standing for
the three bits, with out0 being the least significant one.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{;        +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+}
\NormalTok{;        |                                                         |}
\NormalTok{;        |           +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}\textgreater{} out0}
\NormalTok{;        |           |                +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}\textgreater{} out1}
\NormalTok{;        |           |                |                +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}\textgreater{} out2}
\NormalTok{;        |           |                |                |           |   }
\NormalTok{;        |      +{-}{-}{-}{-}{-}{-}{-}{-}{-}+      +{-}{-}{-}{-}{-}{-}{-}{-}{-}+      +{-}{-}{-}{-}{-}{-}{-}{-}{-}+      |    }
\NormalTok{;        |      |         | car0 |         | car1 |         | car2 |}
\NormalTok{;   inc {-}{-}{-}{-}{-}{-}{-}\textgreater{}| OneBit  |{-}{-}{-}{-}{-}\textgreater{}| OneBit  |{-}{-}{-}{-}{-}\textgreater{}| OneBit  |{-}{-}{-}{-}\textgreater{} |}
\NormalTok{;        |      | Counter |      | Counter |      | Counter |      |}
\NormalTok{; start {-}{-}{-}{-}+{-}{-}\textgreater{}|         |  +{-}{-}\textgreater{}|         |  +{-}{-}\textgreater{}|         |      |}
\NormalTok{;        |  |   +{-}{-}{-}{-}{-}{-}{-}{-}{-}+  |   +{-}{-}{-}{-}{-}{-}{-}{-}{-}+  |   +{-}{-}{-}{-}{-}{-}{-}{-}{-}+      |}
\NormalTok{;        |  +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+                    |}
\NormalTok{;        +{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}{-}+}
\NormalTok{;}
\NormalTok{(define{-}system ThreeBitCounter  :input ( (inc Bool) (start Bool) )}
\NormalTok{ :output ( (out0 Bool) (out1 Bool) (out2 Bool) ) }
\NormalTok{ :local ( (car0 Bool) (car1 Bool) (car2 Bool) ) }
\NormalTok{ :subsys (C1 (OneBitCounter inc start out0 car0))}
\NormalTok{ :subsys (C2 (OneBitCounter car0 start out1 car1)) }
\NormalTok{ :subsys (C3 (OneBitCounter car1 start out2 car2))}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

\paragraph{\texorpdfstring{Sanity requirements on \(I_S\) and
\(T_S\)}{Sanity requirements on I\_S and T\_S}}\label{sanity-requirements-on-i_s-and-t_s}

Because of the infinite trace semantics every system defined in MoXI is
expected to execute forever. This is not a limitation in practice
because systems that are meant to reach a final state can be always
modeled with states that cycle back to themselves and produce stuttering
outputs. In such semantics, the reachability of a \emph{deadlocked
state} (i.e., a state with no successors in the transition relation)
indicates the presence of an error in the system's definition.

Intuitively, for a system definition to define a system with no
deadlocks:

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\item
  Any assignment of values to the input variables can be extended to a
  total assignment (to all the unprimed variables) that satisfies
  \(I_S\).
\item
  For any reachable state \(S\), any assignment \(s\) to the primed
  input variables can be extended to a total assignment \(s'\) so that
  \(s,s'\) satisfies \(T_S\).
\end{enumerate}

The first restriction above guarantees that the system can start at all.
The second ensures that from any reachable state and for any new input
the system can move to another state (\emph{and so} also produce
output).

\begin{itemize}
\item
  A sufficient condition for (1) is that the following formula is valid
  in the (previously specified) background theory:

  \[\forall \boldsymbol{i}\, \exists \boldsymbol{o}\, \exists \boldsymbol{s}\, I_S\]
\item
  A sufficient condition for (2) is that the following formula is valid
  in the background theory:

  \[\forall \boldsymbol{i}~ \forall \boldsymbol{o}~ \forall \boldsymbol{s}~
    \forall \boldsymbol{i'}~
    \exists \boldsymbol{o'}~ \exists \boldsymbol{s'}~ T_S
  \]

  This condition is not necessary, however, since it need not apply to
  unreachable states. Let
  \(\textrm{Reachable}[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{s}]\)
  denote the (possibly higher-order) formula satisfied exactly by the
  reachable states of \(S\). Then, a more accurate sufficient condition
  for (2) above would be the validity of the formula:

  \[\forall \boldsymbol{i}~ \forall \boldsymbol{o}~ \forall \boldsymbol{s}~
    \forall \boldsymbol{i'}~
    \exists \boldsymbol{o'}~ \exists \boldsymbol{s'}~
     \textrm{Reachable} \Rightarrow T_S[\boldsymbol{i}, \boldsymbol{o}, \boldsymbol{s}]
  \]
\end{itemize}

\begin{quote}
\textbf{Note:} In general, checking the two sufficient conditions above
automatically can be impossible or very expensive because of the
quantifier alternations in the conditions.
\end{quote}

\subsubsection{System checking command}\label{system-checking-command}

(check-system \(S\) ~:input ( ( \(i_1\) \(\delta_1\) ) \(\cdots\) (
\(i_m\) \(\delta_m\) ) ) ~:output ( ( \(o_1\) \(\tau_1\) ) \(\cdots\) (
\(o_n\) \(\tau_n\) ) ) ~:local ( ( \(s_1\) \(\sigma_1\) ) \(\cdots\) (
\(s_p\) \(\sigma_p\) ) ) ~:assumption ( \(a\) A ) ~:fairness ( \(f\)
\(F\) ) ~:reachable ( \(r\) \(R\) ) ~:current ( \(c\) \(C\) ) ~:query (
\(q\) ( \(g_1\) \(\cdots\) \(g_q\) ) ) ~:queries ( ( \(q_1\) (
\(g_{1,1}\) \(\cdots\) \(g_{1,n_1}\) ) ) \(\cdots\) ( \(q_t\) (
\(g_{t,1}\) \(\cdots\) \(g_{t,n_t}\) ) ) ) )

where

\begin{itemize}
\tightlist
\item
  \(S\) is the identifier of a previously defined system with \(m\)
  inputs, \(n\) outputs, and \(p\) local variables;
\item
  all attributes are optional and their order is immaterial except that
  :input, :output, :local, have to come before the other attributes
  {[}may not need this restriction{]};
\item
  all attributes except for :input, :output and :local are repeatable.
\item
  \(\boldsymbol{i} = (i_1, \ldots, i_m)\) is a renaming of the
  corresponding input variables of \(S\) of sort
  \(\boldsymbol{\delta} = (\delta_1, \ldots, \delta_m)\);
\item
  \(\boldsymbol{o} = (o_1, \ldots, o_n)\) is a renaming of the
  corresponding output variables of \(S\) of sort
  \(\boldsymbol{\tau} = (\tau_1, \ldots, \tau_n)\);
\item
  \(\boldsymbol{s} = (s_1, \ldots, s_p)\) is a renaming of the
  corresponding local variables of \(S\) of sort
  \(\boldsymbol{\sigma} = (\sigma_1, \ldots, \sigma_p)\);
\item
  \(a\), \(r\), \(f\), \(c\), \(q\), \(q_1, \ldots, q_k\) are
  identifiers;
\item
  \(A\) is (non-temporal) formula over the system variables
  \(\boldsymbol{i}\), \(\boldsymbol{o}\), \(\boldsymbol{s}\), and
  \(\boldsymbol{i'}\) expressing an \emph{environmental assumption} on
  \(\boldsymbol{i'}\);
\item
  \(F\) is (non-temporal) formula over the system variables
  \(\boldsymbol{i}\), \(\boldsymbol{o}\), \(\boldsymbol{s}\), and
  \(\boldsymbol{i'}\) expressing a \emph{fairness condition} on
  \(\boldsymbol{i'}\);
\item
  \(R\) is (non-temporal) formula over all the system variables, primed
  and unprimed, expressing a state \emph{reachability condition};
\item
  \(C\) is (non-temporal) formula over all the unprimed system variables
  expressing a state \emph{initiality condition};
\item
  each \(g_j\) and \(g_{j,k}\) ranges over the \(a\), \(r\), \(f\),
  \(c\) identifiers;
\item
  \((q\ (g_1 \cdots g_q))\) defines a query \(q\) as consisting of the
  formulas named by \(g_1, \dots, g_q\); the same holds for each
  \((q_j\ (g_{j,1} \cdots g_{j,n_j}))\);
\item
  a query can contain more than one assumption, fairness condition and
  reachability condition but at most one initiality condition.
\end{itemize}

\begin{quote}
\textbf{Note:} When the command contains more than one instance of the
attributes :assumption, :reachable, :fairness and :current, the list of
elements of a query \(q\) can refer to any of the identifiers in those
attributes.
\end{quote}

\begin{quote}
\textbf{Note:} The order of the formula names in a query is immaterial.
\end{quote}

\paragraph{Semantics}\label{semantics}

Each query \(q\) (\(q_j\)) in the check-system command asks for the
existence of a trace. The query is to be evaluated with infinite-state
semantics if it includes at least one fairness condition, and the
finite-state semantics otherwise.

Given a check command like the above for a system \(S\), let \(I_S\) and
\(T_S\) be the initial state and transition predicates of \(S\)
\emph{modulo} the variable renamings in the command. The meaning of the
query depends on its components.

Specifically, let \(t, u, v  \geq 0\) :

\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\tightlist
\item
  A \(q\) query of the form ( \(a_1\) \(\cdots\) \(a_t\) \(r_1\)
  \(\cdots\) \(r_u\) ), with each \(a_j\) naming an assumption \(A_j\)
  and each \(r_j\) naming a reachability condition \(R_j\), is
  \emph{satisfiable} iff the formula
\end{enumerate}

\[
\begin{array}{rcl}
  I_S
  & \land & \mathbf{always}\ T_S \\
  & \land & \mathbf{always}\ (A_1 \land \cdots \land A_t) \\
  & \land & \mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u
\end{array}
\]

is \textbf{\(n\)-satisfiable} in LTL for some \(n > 0\).

\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\setcounter{enumi}{1}
\tightlist
\item
  A \(q\) query of the form ( \(c\) \(a_1\) \(\cdots\) \(a_t\) \(r_1\)
  \(\cdots\) \(r_u\) ), with \(c\) naming an initiality condition \(C\),
  each \(a_j\) naming an assumption \(A_j\), and each \(r_j\) naming a
  reachability condition \(R_j\), is \emph{satisfiable} iff the formula
\end{enumerate}

\[
\begin{array}{rcl}
  C
  & \land & \mathbf{always}\ T_S \\
  & \land & \mathbf{always}\ (A_1 \land \cdots \land A_t) \\
  & \land & \mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u
\end{array}
\]

is \textbf{\(n\)-satisfiable} in LTL for some \(n > 0\).

\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\setcounter{enumi}{2}
\tightlist
\item
  A \(q\) query of the form ( \(a_1\) \(\cdots\) \(a_t\) \(r_1\)
  \(\cdots\) \(r_u\) \(f_1\) \(\cdots\) \(f_v\) ), with each \(a_j\)
  naming an assumption \(A_j\), each \(r_j\) naming a reachability
  condition \(R_j\), and each \(f_j\) naming a fairness condition
  \(F_j\), \emph{satisfiable} iff the formula
\end{enumerate}

\[
\begin{array}{rcl}
   I_S
   & \land & \mathbf{always}\ T_S \\
   & \land & \mathbf{always}\ (A_1 \land \cdots \land A_t) \\
   & \land & \mathbf{always}\ \mathbf{eventually}\ F_1 \land \cdots
 \land   \mathbf{always}\ \mathbf{eventually}\ F_v \\
   & \land & \mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u
\end{array}
\]

is \textbf{satisfiable} in LTL.

\begin{enumerate}
\def\labelenumi{(\arabic{enumi})}
\setcounter{enumi}{3}
\tightlist
\item
  A \(q\) query of the form ( \(c\) \(a_1\) \(\cdots\) \(a_t\) \(r_1\)
  \(\cdots\) \(r_u\) \(f_1\) \(\cdots\) \(f_v\) ), with \(c\) naming an
  initiality condition \(C\), each \(a_j\) naming an assumption \(A_j\),
  each \(r_j\) naming a reachability condition \(R_j\), and each \(f_j\)
  naming a fairness condition \(F_j\), \emph{satisfiable} iff the
  formula
\end{enumerate}

\[
\begin{array}{rcl}
   C
   & \land & \mathbf{always}\ T_S \\
   & \land & \mathbf{always}\ (A_1 \land \cdots \land A_t) \\
   & \land & \mathbf{always}\ \mathbf{eventually}\ F_1 \land \cdots
 \land   \mathbf{always}\ \mathbf{eventually}\ F_v \\
   & \land & \mathbf{eventually}\ R_1 \land \cdots \land \mathbf{eventually}\ R_u
\end{array}
\]

is \textbf{satisfiable} in LTL.

Let \(\mathcal T\) be the background theory specified for an MoXI
script. For each satisfiable query in a check-system command, the model
checker is expected to produce

\begin{enumerate}
\def\labelenumi{\arabic{enumi}.}
\tightlist
\item
  a \(\mathcal T\)-interpretation \(\mathcal I\) of the (global) free
  symbols in the script;
\item
  a witnessing trace in \(\mathcal I\).
\end{enumerate}

The interpretation \(\mathcal I\) \emph{must be the same} for all
queries in the same :queries attribute. In contrast, queries in
different attributes may each have their own interpretation of the free
symbols. Regardless of where it occurs, each query may have its own
witnessing trace.

\begin{quote}
\textbf{Note}: To enforce the infinite state semantics for an query it
is enough for it to contain any fairness condition, including the valid
formula true.

\textbf{Note}: For queries with no fairness conditions, the witnessing
trace may not be a trace of the system. {[}Elaborate{]}

\textbf{Note}: The witnessing trace for a query may satisfy each
reachability condition in the query in a different state.
\end{quote}

\paragraph{Check-system examples}\label{check-system-examples}

{[}Non-deterministic arbiter.{]}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(check{-}system NonDetArbiter}
\NormalTok{ :input ( (req1 Bool) (req2 Bool) )}
\NormalTok{ :output ( (gr1 Bool) (gr2 Bool) )}
\NormalTok{ ; There are never concurrent requests}
\NormalTok{ :assumption (a1 (not (and req1 req2)))}
\NormalTok{ ; The same request is never issued twice in a row}
\NormalTok{ :assumption (a2 (and (=\textgreater{} req1 (not req1\textquotesingle{})) (=\textgreater{} req2 (not req2\textquotesingle{}))))}
\NormalTok{ ; Neg of: every request is immediately granted}
\NormalTok{ :reachable (r (not (and (=\textgreater{} req1 gr1) (=\textgreater{} req2 gr2))))}
\NormalTok{ ; check the reachability of r under assumptions a1 and a2}
\NormalTok{ :query (q (a1 a2 r)) }
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

{[}Temporal queries.{]}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(define{-}system Historically :input ((b Bool)) :output ((hb Bool)) }
\NormalTok{ :init (= hb b) }
\NormalTok{ :trans (= hb’ (and b’ hb))}
\NormalTok{)}

\NormalTok{(define{-}system Before :input ((b Bool)) :output ((bb Bool)) }
\NormalTok{ :init (= bb\textquotesingle{} false) }
\NormalTok{ :trans (= bb’ b)}
\NormalTok{)}

\NormalTok{(define{-}system Count :input ((b Bool)) :output ((c Int)) }
\NormalTok{ :init (= c (ite b 1 0))}
\NormalTok{ :trans (= c’ (+ c (ite b 0 1)))}
\NormalTok{)}

\NormalTok{(define{-}system Monitor :input ((r1 Bool) (r2 Bool)) :output ((g1 Bool) (g2 Bool))  }
\NormalTok{ :local ((a1 Bool) (a2 Bool) (b Bool) (h1 Bool) (h2 Bool) (bf Bool) (c1 Int))}
\NormalTok{ :subsys (A (NonDetArbiter r1 r2 g1 g2))}
\NormalTok{ :subsys (H1 (Historically a1 h1))}
\NormalTok{ :subsys (H2 (Historically a2 h2))}
\NormalTok{ :subsys (C (Count g1 c1))}
\NormalTok{ :subsys (B (Before b bf))}
\NormalTok{ :inv (and}
\NormalTok{   ; a1 \textless{}=\textgreater{} no requests}
\NormalTok{   (= a1 (and (not r1) (not r2)))}
\NormalTok{   ; a2 \textless{}=\textgreater{} no grants}
\NormalTok{   (= a2 (and (not g1) (not g2)))}
\NormalTok{   ; b \textless{}=\textgreater{} c1 is 4}
\NormalTok{   (= b (= c1 4))}
\NormalTok{ )}
\NormalTok{)}

\NormalTok{(check{-}system Monitor :input ((r1 Bool) (r2 Bool)) :output ((g1 Bool) (g2 Bool))}
\NormalTok{ :local ((a1 Bool) (a2 Bool) (b Bool) (h1 Bool) (h2 Bool) (bf Bool) (c1 Int))}
\NormalTok{ ; no concurrent requests}
\NormalTok{ :assumption (A (not (and r1 r2))) }
\NormalTok{ ; neg of: if there have been no requests, there have been no grants }
\NormalTok{ :reachable (P1 (not (=\textgreater{} h1 h2))) }
\NormalTok{ ; neg of: a request is granted at most 4 times}
\NormalTok{ :reachable (P2 (not (=\textgreater{} bf (not g1)))) }
\NormalTok{ :query (Q1 (A P1))}
\NormalTok{ :query (Q2 (A P2))}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

\paragraph{Check-system response}\label{check-system-response}

We define a trail each to be a finite sequence of states. A trace
consists of two trails:

\begin{itemize}
\tightlist
\item
  a prefix trail and
\item
  a lasso trail.
\end{itemize}

A trace represents an infinite counterexample and consists of a finite
prefix of type trail followed by a lasso of type trail representing an
infinite loop: there is a transition from last state of the lasso to its
first state. Oppositely from a trace, a certificate represents a proof
of correctness. We return one trail or certificate in response to each
query.

\textbf{Verbose} response with input var \texttt{i}, output var
\texttt{o}, local var \texttt{s}, reachability pred \texttt{r}, and
fairness condition \texttt{f}.

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(check{-}system{-}response}
\NormalTok{ :verbosity full}
\NormalTok{ :query (q1 :result sat :model m :trace t)}
\NormalTok{ :query (q2 :result unsat :certificate c)}
\NormalTok{ :query (q3 :result unknown)                         }\CommentTok{; for timeouts and other cases}
\NormalTok{ :trace (t :prefix p :lasso l)                       }\CommentTok{; t = pl\^{}ω}
\NormalTok{ :model (m M)                                        }\CommentTok{; M is model in SMT{-}LIB format}
\NormalTok{ :trail (p ( (}\DecValTok{0}\NormalTok{ (i i₀) (o o₀) (s s₀) (r r₀) (f f₀))  }\CommentTok{; numbered state/valuation}
              \OperatorTok{...}
\NormalTok{             (j (i iⱼ) (o oⱼ) (s sⱼ) (r rⱼ) (f fⱼ))}
\NormalTok{           )}
\NormalTok{        ) }
\NormalTok{ :trail (l ( ( }\OperatorTok{...}\NormalTok{ ) }\OperatorTok{...}\NormalTok{ ( }\OperatorTok{...}\NormalTok{ ) ))}
\NormalTok{ :certificate (c :inv F :k n)}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}

The \textbf{compact} response format is identical to the verbose one
except that each trail starts with a fully specified state and continues
with states that list only the variables whose value differs from their
value in the previous state.

{[}Complete examples{]}

\begin{Shaded}
\begin{Highlighting}[]
\NormalTok{(check{-}system{-}response}
\NormalTok{ :verbosity compact}
 \OperatorTok{...}
\NormalTok{)}
\end{Highlighting}
\end{Shaded}


\end{document}
