Skip to content
Permalink
Browse files

Fix While timeout in Isabelle semantics

  • Loading branch information...
palas committed Apr 14, 2019
1 parent b626bfb commit 7a5749d8cfcea411e2b4553a75e913faf9eebcea
Showing with 1 addition and 1 deletion.
  1. +1 −1 semantics-2.0/formalisation/Semantics.thy
@@ -563,7 +563,7 @@ function reduceRec :: "BlockNumber \<Rightarrow> State \<Rightarrow> Environment
(Constant (evalValue blockNum state def))
(reduceRec blockNum state env contract)" |
"reduceRec blockNum state env (While obs timeout contractWhile contractAfter) =
(if isExpired timeout blockNum
(if isExpired blockNum timeout
then reduceRec blockNum state env contractAfter
else (if evalObservation blockNum state obs
then (While obs timeout (reduceRec blockNum state env contractWhile) contractAfter)

0 comments on commit 7a5749d

Please sign in to comment.
You can’t perform that action at this time.