Commit efc6e4d3 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

sec def

parent 82c518a1
......@@ -97,10 +97,11 @@ G (out=NO_CONN ->
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (inp=CH_OPEN & out!=CH_MAX -> (inp=CH_OPEN -> out=CH_MAX)
W (inp=CH_CLOSE & out!=CH_NONE &
(isConnectionInput(in) -> out=CH_NONE)
W (inp=CH_OPEN) ) )
G (inp=CH_OPEN & out!=CH_MAX ->
(inp=CH_OPEN -> out=CH_MAX)
W (inp=CH_CLOSE & out!=CH_NONE &
(isConnectionInput(in) -> out=CH_NONE)
W (inp=CH_OPEN) ) )
\end{lstlisting}
\caption{Mapper induced property.}
\label{prop:channel}
......
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