Commit 8f443ec0 authored by Ralf Jung's avatar Ralf Jung

temporary link to prophecy MR, until we can reference a paper instead

parent e262cd8e
Pipeline #17530 passed with stage
in 13 minutes and 54 seconds
\section{Language}
\label{sec:language}
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), a set $\Obs$ of \emph{observations} (or ``observable events'') and a set $\State$ of \emph{states} (metavariable $\state$) such that
A \emph{language} $\Lang$ consists of a set \Expr{} of \emph{expressions} (metavariable $\expr$), a set \Val{} of \emph{values} (metavariable $\val$), a set $\Obs$ of \emph{observations}\footnote{See \url{https://gitlab.mpi-sws.org/iris/iris/merge_requests/173} for how observations are useful to encode prophecy variables.} (or ``observable events'') and a set $\State$ of \emph{states} (metavariable $\state$) such that
\begin{itemize}[itemsep=0pt]
\item There exist functions $\ofval : \Val \to \Expr$ and $\toval : \Expr \pfn \Val$ (notice the latter is partial), such that
\begin{mathpar}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment