diff --git a/Elixir.hs b/Elixir.hs index 43d0033..ea92e7b 100644 --- a/Elixir.hs +++ b/Elixir.hs @@ -73,26 +73,27 @@ actionsAndConditions g (ActionOr as) = let (ics, ias) = unzipAndFold (map (actio in (if allUnchanged as then ["false"] else [orFold ics], if ias == [] then [] else [decide g as]) -- (IF) -actionsAndConditions g (If p t e) = let cp = predicate g p - (ct, at) = actionsAndConditions g t - (ce, ae) = actionsAndConditions g e - c = ifExpr cp (if isUnchanged t then "false" else cFold ct) (if isUnchanged e then "false" else cFold ce) - a = ifExpr cp (aFold at) (aFold ae) - in ([c], [a]) +actionsAndConditions g (ActionIf p t e) = let cp = value g p + (ct, at) = actionsAndConditions g t + (ce, ae) = actionsAndConditions g e + c = ifExpr cp (if isUnchanged t then "false" else cFold ct) (if isUnchanged e then "false" else cFold ce) + a = ifExpr cp (aFold at) (aFold ae) + in ([c], [a]) -- (COND) -actionsAndConditions g (Condition p) = ([predicate g p], []) +actionsAndConditions g (Condition p) = ([value g p], []) -- [new] (EXT) -actionsAndConditions g (Exists i v (ActionOr as)) = let ig = (i, "param"):g - (ics, _) = unzipAndFold (map (actionsAndConditions ig) as) - c = "Enum.any?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ orFold ics ++ "end\n)" - in ([c], [decide g [Exists i v (ActionOr as)]]) +actionsAndConditions g (Exists i v a) = let ig = (i, "param"):g + (ics, _) = actionsAndConditions ig a + c = "Enum.any?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)" + in ([c], [decide g [a]]) + -- [new]: must test -actionsAndConditions g (ForAll i v (ActionAnd as)) = let ig = (i, "param"):g - (ics, ias) = unzipAndFold (map (actionsAndConditions ig) as) - c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)" - in ([c], ias) +actionsAndConditions g (ForAll i v a) = let ig = (i, "param"):g + (ics, ias) = actionsAndConditions ig a + c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ "end\n)" + in ([c], ias) -- (TRA) actionsAndConditions g a = ([], [action g a]) @@ -115,89 +116,49 @@ action _ (Unchanged is) = let u = \i -> snake i ++ ": variables[:" ++ snake i + in "%{ " ++ intercalate ",\n" (map u is) ++ " }" -- [new] needs testing -action g (Value v) = value g v +-- action g (Value v) = value g v + +action _ a = error("Missing action case: " ++ show a) -action _ a = error(show a) {-- \vdash_p --} -predicate :: Context -> Predicate -> ElixirCode +value :: Context -> Value -> ElixirCode -- (PRED-EQ) -predicate g (Equality v1 v2) = value g v1 ++ " == " ++ value g v2 +value g (Equality v1 v2) = value g v1 ++ " == " ++ value g v2 -- (PRED-INEQ) -predicate g (Inequality v1 v2) = value g v1 ++ " != " ++ value g v2 +value g (Inequality v1 v2) = value g v1 ++ " != " ++ value g v2 -- Similar rules -predicate g (Gt v1 v2) = value g v1 ++ " > " ++ value g v2 -predicate g (Lt v1 v2) = value g v1 ++ " < " ++ value g v2 -predicate g (Gte v1 v2) = value g v1 ++ " >= " ++ value g v2 -predicate g (Lte v1 v2) = value g v1 ++ " <= " ++ value g v2 +value g (Gt v1 v2) = value g v1 ++ " > " ++ value g v2 +value g (Lt v1 v2) = value g v1 ++ " < " ++ value g v2 +value g (Gte v1 v2) = value g v1 ++ " >= " ++ value g v2 +value g (Lte v1 v2) = value g v1 ++ " <= " ++ value g v2 -- [new] (PRED-CALL) -predicate g (ConditionCall i ps) = call (i ++ "Condition") ("variables":map (value g) ps) +value g (ConditionCall i ps) = call (i ++ "Condition") ("variables":map (value g) ps) -- (PRED-IN) -predicate g (RecordBelonging v1 v2) = "Enum.member?(" ++ value g v2 ++ ", " ++ value g v1 ++ ")" +value g (RecordBelonging v1 v2) = "Enum.member?(" ++ value g v2 ++ ", " ++ value g v1 ++ ")" -- [new] (PRED-NOTIN) -predicate g (RecordNotBelonging v1 v2) = "not " ++ predicate g (RecordBelonging v1 v2) +value g (RecordNotBelonging v1 v2) = "not " ++ value g (RecordBelonging v1 v2) -- (PRED-NOT) -predicate g (Not p) = "not " ++ predicate g p +value g (Not p) = "not " ++ value g p -- [new] (PRED-AND) -predicate g (And ps) = intercalate " and " (map (predicate g) ps) +value g (And ps) = intercalate " and " (map (value g) ps) -- [new] (PRED-OR) -predicate g (Or ps) = intercalate " or " (map (predicate g) ps) - --- [new] (PRED-ALL) -predicate g (PForAll i v p) = "Enum.all?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ predicate ((i, "param"):g) p ++ " end)" - -predicate _ p = error("Missing predicate case: " ++ show p) - -{-- \vdash_init --} -initialState :: Context -> Action -> ElixirCode - --- (INIT-AND) -initialState g (ActionAnd as) = aFold (map (initialState g) as) - --- (INIT-EQ) -initialState g (Condition (Equality (Ref i) v)) = "%{ " ++ snake i ++ ": " ++ value g v ++ " }" - --- Restriction -initialState _ p = error("Init condition ambiguous: " ++ show p) - --- Comment extraction -ini g (ActionDefinition _ _ doc a) = comment doc ++ initialState g a - - -{-- \vdash_next --} -next :: Context -> Definition -> ElixirCode - --- (NEXT) -next g (ActionDefinition _ _ doc a) = let (_, actions) = actionsAndConditions g a - in funDoc doc ++ "def main(variables) do\n" ++ ident (logState ++ "main(" ++ (aFold actions)) ++ ")\nend\n" - - -{-- \vdash_i -} -actionInfo :: Context -> Action -> ElixirCode --- (INFO-EX) -actionInfo g (Exists i v (ActionOr as)) = let ig = (i, "param"):g - l = map (actionInfo ig) as - s = intercalate ",\n" l - in "Enum.map(" ++ value ig v ++ ", fn (" ++ i ++ ") -> [\n" ++ ident s ++ "\n] end\n)" +value g (Or ps) = intercalate " or " (map (value g) ps) --- (INFO-DEF) -actionInfo g a = let (cs, as) = actionsAndConditions g a - n = "action: \"" ++ actionName a ++ "\"" - c = "condition: " ++ cFold cs - s = "state: " ++ aFold as - in "%{ " ++ intercalate ", " [n,c,s] ++ " }" +value g (If c t e) = "if " ++ value g c ++ ", do: " ++ value g t ++ ", else: " ++ value g e +-- [new] (PRED-ALL) +value g (PForAll i v p) = "Enum.all?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)" -{-- \vdash_v --} -value :: Context -> Value -> ElixirCode +value g (PExists i v p) = "Enum.any?(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)" -- (REC-INDEX) value g (Index v k) = value g v ++ "[" ++ value g k ++ "]" @@ -211,11 +172,15 @@ value g (Union s (Set [v])) = "MapSet.put(" ++ value g s ++ ", " ++ value g v ++ value g (Union s1 s2) = "MapSet.union(" ++ value g s1 ++ ", " ++ value g s2 ++ ")" -- [new] (SET-FILT) -value g (Filtered i v p) = "Enum.filter(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ predicate ((i, "param"):g) p ++ " end)" +value g (Filtered i v p) = "Enum.filter(" ++ value g v ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) p ++ " end)" -- [new] (SET-CAR) value g (Cardinality s) = "Enum.count(" ++ value g s ++ ")" +value g (SetIn v s) = "MapSet.member?(" ++ value g s ++ ", " ++ value g v ++ ")" + +value g (SetMinus s1 s2) = "MapSet.difference?(" ++ value g s1 ++ ", " ++ value g s2 ++ ")" + -- (REC-LIT) and (REC-EX), aggregated to ensure ordering value g (Record rs) = let (literals, generations) = partition isLiteral rs m = intercalate " ++ " (map (mapping g) generations) -- merge @@ -225,16 +190,15 @@ value g (Record rs) = let (literals, generations) = partition isLiteral rs -- (REC-EXCEPT) value g (Except i es) = unlines (map (\(k,v) -> "Map.put(" ++ reference g i ++ ", " ++ value g k ++ ", " ++ value g v ++ ")") es) +value g (FunGen i s v) = "MapSet.new(" ++ value g s ++ ", fn(" ++ i ++ ") -> " ++ value ((i, "param"):g) v ++ " end)" + -- [new] (CASE) value g (Case ms) = "cond do\n" ++ intercalate "\n" (map (caseMatch g) ms) ++ "\nend\n" -- Others, not specified -value _ (Str s) = show s value g (Range n1 n2) = value g n1 ++ ".." ++ value g n2 -value _ (Boolean b) = if b then "true" else "false" value g (Ref i) = reference g i value g (Tuple as) = "{" ++ intercalate ", " (map (value g) as) ++ "}" -value _ (Num d) = show d value g (Neg a) = "-" ++ value' g a value g (Add a b) = value' g a ++ " + " ++ value' g b value g (Sub a b) = value' g a ++ " - " ++ value' g b @@ -242,17 +206,60 @@ value g (Mul a b) = value' g a ++ " * " ++ value' g b value g (Div a b) = value' g a ++ " / " ++ value' g b value g (Mod a b) = "rem(" ++ value' g a ++ ", " ++ value' g b ++ ")" value g (Domain v) = "Map.keys(" ++ value g v ++ ")" +value _ (Lit l) = lit l value _ v = error("Missing value case: " ++ show v) -value' _ (Num d) = show d +value' _ (Lit (Num d)) = show d value' g (Ref i) = reference g i value' g e = "(" ++ value g e ++ ")" +lit (Str s) = show s +lit (Num d) = show d +lit (Boolean b) = if b then "true" else "false" + +{-- \vdash_init --} +initialState :: Context -> Value -> ElixirCode + +-- (INIT-AND) +initialState g (And as) = aFold (map (initialState g) as) + +-- (INIT-EQ) +initialState g (Equality (Ref i) v) = "%{ " ++ snake i ++ ": " ++ value g v ++ " }" + +-- Restriction +initialState _ p = error("Init condition ambiguous: " ++ show p) + +-- Comment extraction +ini g (ActionDefinition _ _ doc (Condition a)) = comment doc ++ initialState g a + + +{-- \vdash_next --} +next :: Context -> Definition -> ElixirCode + +-- (NEXT) +next g (ActionDefinition _ _ doc a) = let (_, actions) = actionsAndConditions g a + in funDoc doc ++ "def main(variables) do\n" ++ ident (logState ++ "main(" ++ (aFold actions)) ++ ")\nend\n" + + +{-- \vdash_i -} +actionInfo :: Context -> Action -> ElixirCode +-- (INFO-EX) +actionInfo g (Exists i v (ActionOr as)) = let ig = (i, "param"):g + l = map (actionInfo ig) as + s = intercalate ",\n" l + in "Enum.map(" ++ value ig v ++ ", fn (" ++ i ++ ") -> [\n" ++ ident s ++ "\n] end\n)" + +-- (INFO-DEF) +actionInfo g a = let (cs, as) = actionsAndConditions g a + n = "action: \"" ++ actionName a ++ "\"" + c = "condition: " ++ cFold cs + s = "state: " ++ aFold as + in "%{ " ++ intercalate ", " [n,c,s] ++ " }" -caseMatch g (Match p v) = predicate g p ++ " -> " ++ value g v +caseMatch g (Match p v) = value g p ++ " -> " ++ value g v caseMatch g (DefaultMatch v) = "true -> " ++ value g v -mapping g ((Key i), v) = snake i ++ ": " ++ value g v +mapping g ((Key i), v) = show i ++ ": " ++ value g v mapping g ((All i a), v) = let ig = (i, "param"):g in value g a ++ " |> Enum.map(fn (" ++ i ++ ") -> {" ++ i ++ ", " ++ value ig v ++ "} end)" -- (VAL-*) diff --git a/Head.hs b/Head.hs index af181d3..e9c9a39 100644 --- a/Head.hs +++ b/Head.hs @@ -21,32 +21,55 @@ data Definition = ActionDefinition Identifier [Parameter] Documentation Action | Comment String deriving(Show, Eq) -data Key = Key Identifier | All Identifier Value deriving(Show, Eq) - -data CaseMatch = Match Predicate Value | DefaultMatch Value deriving(Show, Eq) - -data Predicate = Equality Value Value | Inequality Value Value - | Gt Value Value | Lt Value Value - | Gte Value Value | Lte Value Value - | RecordBelonging Value Value - | RecordNotBelonging Value Value - | And [Predicate] - | Or [Predicate] - | Not Predicate - | ConditionCall Identifier [Value] - | PExists Identifier Value Predicate - | PForAll Identifier Value Predicate - deriving(Show, Eq) - -data Action = Condition Predicate | Value Value | Primed Identifier Value | Unchanged [Identifier] | ActionNot Action - | ActionAnd [Action] | ActionOr [Action] | ActionCall Identifier [Value] - | If Predicate Action Action | Exists Identifier Value Action | ForAll Identifier Value Action deriving(Show, Eq) - -data Value = Set [Value] | Tuple [Value] | FunSet Value Value | FunGen Identifier Value Value | SetTimes Value Value - | Union Value Value | Filtered Identifier Value Predicate | Cardinality Value - | Record [(Key, Value)] | Except Identifier [(Value, Value)] | Case [CaseMatch] | Domain Value - | Str String | Boolean Bool | FullSet String | Index Value Value | Range Value Value - | Num Integer +data Lit = Str String | Boolean Bool | Num Integer | FullSet String deriving(Show, Eq) + +data Key = Key Lit | All Identifier Value deriving(Show, Eq) + +data CaseMatch = Match Value Value | DefaultMatch Value deriving(Show, Eq) + +data Action = Condition Value + | Primed Identifier Value + | Unchanged [Identifier] + | ActionNot Action + | ActionAnd [Action] + | ActionOr [Action] + | ActionCall Identifier [Value] + | ActionIf Value Action Action + | Exists Identifier Value Action + | ForAll Identifier Value Action + deriving(Show, Eq) + +data Value = Equality Value Value + | Inequality Value Value + | Gt Value Value | Lt Value Value + | Gte Value Value | Lte Value Value + | RecordBelonging Value Value + | RecordNotBelonging Value Value + | And [Value] + | Or [Value] + | Not Value + | If Value Value Value + | ConditionCall Identifier [Value] + | PExists Identifier Value Value + | PForAll Identifier Value Value + | Let [Definition] Value + | Set [Value] + | Tuple [Value] + | FunSet Value Value + | FunGen Identifier Value Value + | SetTimes Value Value + | SetIn Value Value + | SetMinus Value Value + | Union Value Value + | Filtered Identifier Value Value + | Cardinality Value + | Record [(Key, Value)] + | RecordSet [(Key, Value)] + | Except Identifier [(Value, Value)] + | Case [CaseMatch] + | Domain Value + | Index Value Value + | Range Value Value | Ref String | Neg Value | Add Value Value @@ -54,4 +77,5 @@ data Value = Set [Value] | Tuple [Value] | FunSet Value Value | FunGen Identifie | Mul Value Value | Div Value Value | Mod Value Value + | Lit Lit deriving (Show, Eq) diff --git a/Helpers.hs b/Helpers.hs index aea06b9..c54c7ef 100644 --- a/Helpers.hs +++ b/Helpers.hs @@ -71,7 +71,7 @@ mapMerge (m:ms) = "Map.merge(\n " ++ m ++ ",\n" ++ ident (mapMerge ms) ++ ")\n" preassignment as = (head as) == '(' || take 2 as == "if" || dropWhile (/= ':') as == [] || take 4 as == "Enum" || take 3 as == "Map" || take 4 as == "List" -interpolate (Str i) = "#{inspect " ++ i ++ "}" +interpolate (Lit (Str i)) = "#{inspect " ++ i ++ "}" interpolate (Ref i) = "#{inspect " ++ i ++ "}" interpolate i = show i @@ -113,5 +113,4 @@ findVariables ds = concat (map (\d -> case d of {Variables cs -> cs; _ -> [] }) findIdentifier i ds = case find (isNamed i) ds of Just a -> a - Nothing -> error("Definition not found: " ++ (show i)) - + Nothing -> error("Definition not found: " ++ show i ++ " in " ++ show ds) diff --git a/JSONParser.hs b/JSONParser.hs index b2189a0..4955e86 100644 --- a/JSONParser.hs +++ b/JSONParser.hs @@ -10,6 +10,7 @@ import Data.List import GHC.Generics import qualified Data.ByteString.Lazy as B import Control.Applicative +import Control.Arrow type Kind = String @@ -21,7 +22,7 @@ data Spec = Spec [Module] deriving (Show,Generic) data Module = Module String [Declaration] deriving (Show, Generic) data Declaration = Declaration Kind String (Maybe Expression) | Ignored deriving (Show, Generic) -data Expression = Expression Kind (Maybe String) (Maybe [Expression]) (Maybe String) (Maybe TlaValue) deriving (Show, Generic) +data Expression = ValEx TlaValue | NameEx String | OperEx String [Expression] | LetInEx [Declaration] Expression deriving (Show, Generic) data TlaValue = TlaStr String | TlaBool Bool | TlaInt Integer | FullSet String deriving (Show, Generic) instance FromJSON Spec where @@ -37,8 +38,11 @@ instance FromJSON Module where instance FromJSON Declaration where parseJSON = withObject "Declaration" $ \obj -> do - src <- obj .: "source" >>= (.: "filename") - case src :: String of + src <- obj .: "source" + filename <- case src of + Object a -> a .: "filename" + _ -> return "UNKNOWN" + case filename :: String of "Functions" -> return Ignored "SequencesExt" -> return Ignored _ -> do k <- obj .: "kind" @@ -59,11 +63,14 @@ instance FromJSON TlaValue where _ -> fail ("Unknown value kind: " ++ valueKind) instance FromJSON Expression where - parseJSON = withObject "Expression" $ \obj -> Expression <$> obj .: "kind" - <*> obj .:? "oper" - <*> obj .:? "args" - <*> obj .:? "name" - <*> obj .:? "value" + parseJSON = withObject "Expression" $ \obj -> do + exprKind <- obj .: "kind" + case exprKind :: String of + "ValEx" -> fmap ValEx (obj .: "value") + "NameEx" -> fmap NameEx (obj .: "name") + "OperEx" -> liftA2 OperEx (obj .: "oper") (obj .: "args") + "LetInEx" -> liftA2 LetInEx (obj .: "decls") (obj .: "body") + _ -> fail ("Unknown expression kind: " ++ exprKind) notIgnored Ignored = False notIgnored _ = True @@ -83,170 +90,140 @@ convertDefinitions (Declaration k n body) = case body of convertBody :: Kind -> String -> Expression -> Either String H.Definition convertBody k i e = case k of "OperEx" -> Right (H.Comment "A") - "TlaOperDecl" -> convertExpression e >>= \x -> Right (H.ActionDefinition i [] [] x) + "TlaOperDecl" -> if isTemporal e then Right (H.Comment (show e)) else convertExpression e >>= \x -> Right (H.ActionDefinition i [] [] x) + "TlaAssumeDecl" -> Right (H.Comment (show e)) _ -> Left ("Unknown body kind " ++ show k) primed :: Expression -> Either String H.Identifier -primed (Expression k o as i v) = case o of - Just "PRIME" -> case as of - Just [a] -> identifier a - Nothing -> Left "Missing name in NameEx" +primed (OperEx o [a]) = case o of + "PRIME" -> identifier a + _ -> Left ("Not prime operator: " ++ o) identifier :: Expression -> Either String H.Identifier -identifier (Expression k o as i v) = if k == "NameEx" then case i of - Just s -> Right s - Nothing -> Left "Missing name in NameEx" - else Left ("Missing identifier in " ++ show (Expression k o as i v)) +identifier (NameEx i) = Right i +identifier e = Left ("Expected name expression when looking for identifier, got: " ++ show e) manyIdentifiers :: Expression -> Either String [H.Identifier] -manyIdentifiers (Expression k o as i v) = case k of - "NameEx" -> fmap (:[]) (identifier (Expression k o as i v)) - "OperEx" -> if o == Just "TUPLE" then case as of - Just es -> mapM identifier es - Nothing -> Left ("Missing args in " ++ show (Expression k o as i v)) - else Left ("Missing identifier in " ++ show (Expression k o as i v)) - -identifierFromString :: Expression -> Either String H.Identifier -identifierFromString (Expression k o as i v) = if k == "ValEx" then case v of - Just (TlaStr s) -> Right s - _ -> Left ("Expected string for identifier " ++ show v) - else Left ("Missing identifier in " ++ show (Expression k o as i v)) - -ref :: Maybe String -> Either String H.Value -ref (Just v) = Right (H.Ref v) -ref x = Left ("Not a reference: " ++ show x) - -val :: Maybe TlaValue -> Either String H.Value -val (Just(TlaStr s)) = Right (H.Str s) -val (Just(TlaBool b)) = Right (H.Boolean b) -val (Just(TlaInt n)) = Right (H.Num n) -val (Just (FullSet s)) = Right (H.FullSet s) -val Nothing = Left "Value not found" +manyIdentifiers (NameEx i) = Right [i] +manyIdentifiers (OperEx o as) = case o of + "TUPLE" -> mapM identifier as + _ -> Left ("Not tuple operator: " ++ o) + +val :: TlaValue -> H.Lit +val (TlaStr s) = H.Str s +val (TlaBool b) = H.Boolean b +val (TlaInt n) = H.Num n +val (FullSet s) = H.FullSet s splits :: [a] -> [(a, a)] splits [a, b] = [(a, b)] splits (a:b:ts) = (a,b):splits ts -valueOperators :: [String] -valueOperators = ["TUPLE", "MINUS", "PLUS", "EXCEPT", "DOMAIN", "RECORD"] - -valuePrefixes :: [String] -valuePrefixes = ["FUN_", "SET_", "INT_"] - convertValue :: Expression -> Either String H.Value -convertValue (Expression k o as i v) = case k of - "NameEx" -> ref i - "ValEx" -> val v - "OperEx" -> case o of - Just "FUN_SET" -> case as of - Just [a1, a2] -> liftA2 H.FunSet (convertValue a1) (convertValue a2) - Just "FUN_APP" -> case as of - Just [a1, a2] -> liftA2 H.Index (convertValue a1) (convertValue a2) - Just "FUN_CTOR" -> case as of - Just [a1, a2, a3] -> liftA3 H.FunGen (identifier a1) (convertValue a2) (convertValue a3) - Just "SET_TIMES" -> case as of - Just [a1, a2] -> liftA2 H.SetTimes (convertValue a1) (convertValue a2) - Just "SET_ENUM" -> case as of - Just vs -> fmap H.Set (mapM convertValue vs) - Just "INT_RANGE" -> case as of - Just [a1, a2] -> liftA2 H.Range (convertValue a1) (convertValue a2) - Just "TUPLE" -> case as of - Just vs -> fmap H.Tuple (mapM convertValue vs) - Just "RECORD" -> case as of - Just vs -> fmap H.Record (convertRecordValues vs) - Just "MINUS" -> case as of - Just [a1, a2] -> liftA2 H.Sub (convertValue a1) (convertValue a2) - Just "PLUS" -> case as of - Just [a1, a2] -> liftA2 H.Add (convertValue a1) (convertValue a2) - Just "EXCEPT" -> case as of - Just (e:es) -> liftA2 H.Except (identifier e) (fmap splits (mapM convertValue es)) - Just "DOMAIN" -> case as of - Just [a1] -> fmap H.Domain (convertValue a1) - Just op -> Left ("Unknown value operator " ++ op) - _ -> Left ("Unknown value kind " ++ k) - -convertPredicate :: Expression -> Either String H.Predicate -convertPredicate (Expression k o as i v) = case k of - "OperEx" -> case o of - Just "NE" -> case as of - Just [x1, x2] -> liftA2 H.Inequality (convertValue x1) (convertValue x2) - Just "EQ" -> case as of - Just [x1, x2] -> liftA2 H.Equality (convertValue x1) (convertValue x2) - Just "GT" -> case as of - Just [x1, x2] -> liftA2 H.Gt (convertValue x1) (convertValue x2) - Just "GE" -> case as of - Just [x1, x2] -> liftA2 H.Gte (convertValue x1) (convertValue x2) - Just "EXISTS3" -> case as of - Just [a1, a2, a3] -> liftA3 H.PExists (identifier a1) (convertValue a2) (convertPredicate a3) - Just "FORALL3" -> case as of - Just [a1, a2, a3] -> liftA3 H.PForAll (identifier a1) (convertValue a2) (convertPredicate a3) - Just "AND" -> case as of - Just es -> fmap H.And (mapM convertPredicate es) - Just "OR" -> case as of - Just es -> fmap H.Or (mapM convertPredicate es) - Just "NOT" -> case as of - Just [a] -> fmap H.Not (convertPredicate a) - Just "OPER_APP" -> case as of - Just (e:es) -> liftA2 H.ConditionCall (identifier e) (mapM convertValue es) - _ -> Left ("Unknown predicate operator " ++ show o ++ " in " ++ show (Expression k o as i v)) - _ -> Left("Unknown predicate kind " ++ k) +convertValue (NameEx i) = Right(H.Ref i) +convertValue (ValEx v) = Right(H.Lit (val v)) +convertValue (OperEx o as) = let r = case o of + "FUN_SET" -> case as of + [a1, a2] -> liftA2 H.FunSet (convertValue a1) (convertValue a2) + "FUN_APP" -> case as of + [a1, a2] -> liftA2 H.Index (convertValue a1) (convertValue a2) + "FUN_CTOR" -> case as of + [a1, a2, a3] -> liftA3 H.FunGen (identifier a2) (convertValue a3) (convertValue a1) + "SET_TIMES" -> case as of + [a1, a2] -> liftA2 H.SetTimes (convertValue a1) (convertValue a2) + "SET_ENUM" -> case as of + vs -> fmap H.Set (mapM convertValue vs) + "SET_IN" -> case as of + [a1, a2] -> liftA2 H.SetIn (convertValue a1) (convertValue a2) + "SET_MINUS" -> case as of + [a1, a2] -> liftA2 H.SetMinus (convertValue a1) (convertValue a2) + "SET_FILTER" -> case as of + [a1, a2, a3] -> liftA3 H.Filtered (identifier a1) (convertValue a2) (convertValue a3) + "INT_RANGE" -> case as of + [a1, a2] -> liftA2 H.Range (convertValue a1) (convertValue a2) + "TUPLE" -> case as of + vs -> fmap H.Tuple (mapM convertValue vs) + "RECORD" -> case as of + vs -> fmap H.Record (convertRecordValues vs) + "RECORD_SET" -> case as of + vs -> fmap H.RecordSet (convertRecordValues vs) + "MINUS" -> case as of + [a1, a2] -> liftA2 H.Sub (convertValue a1) (convertValue a2) + "PLUS" -> case as of + [a1, a2] -> liftA2 H.Add (convertValue a1) (convertValue a2) + "EXCEPT" -> case as of + (e:es) -> liftA2 H.Except (identifier e) (fmap splits (mapM convertValue es)) + "DOMAIN" -> case as of + [a1] -> fmap H.Domain (convertValue a1) + "NE" -> case as of + [x1, x2] -> liftA2 H.Inequality (convertValue x1) (convertValue x2) + "EQ" -> case as of + [x1, x2] -> liftA2 H.Equality (convertValue x1) (convertValue x2) + "GT" -> case as of + [x1, x2] -> liftA2 H.Gt (convertValue x1) (convertValue x2) + "LT" -> case as of + [x1, x2] -> liftA2 H.Lt (convertValue x1) (convertValue x2) + "GE" -> case as of + [x1, x2] -> liftA2 H.Gte (convertValue x1) (convertValue x2) + "LE" -> case as of + [x1, x2] -> liftA2 H.Lte (convertValue x1) (convertValue x2) + "EXISTS3" -> case as of + [a1, a2, a3] -> liftA3 H.PExists (identifier a1) (convertValue a2) (convertValue a3) + "FORALL3" -> case as of + [a1, a2, a3] -> liftA3 H.PForAll (identifier a1) (convertValue a2) (convertValue a3) + "AND" -> case as of + es -> fmap H.And (mapM convertValue es) + "OR" -> case as of + es -> fmap H.Or (mapM convertValue es) + "NOT" -> case as of + [a] -> fmap H.Not (convertValue a) + "IF_THEN_ELSE" -> case as of + [a1, a2, a3] -> liftA3 H.If (convertValue a1) (convertValue a2) (convertValue a3) + "OPER_APP" -> case as of + (e:es) -> liftA2 H.ConditionCall (identifier e) (mapM convertValue es) + op -> Left ("Unknown value operator " ++ op) + in left (\s -> s ++ "\nwhen converting " ++ show (OperEx o as)) r +convertValue (LetInEx ds b) = liftA2 H.Let (mapM convertDefinitions ds) (convertValue b) convertAction :: Expression -> Either String H.Action -convertAction (Expression k o as i v) = case k of - "OperEx" -> case o of - Just "EXISTS3" -> case as of - Just [a1, a2, a3] -> liftA3 H.Exists (identifier a1) (convertValue a2) (convertExpression a3) - Just "FORALL3" -> case as of - Just [a1, a2, a3] -> liftA3 H.ForAll (identifier a1) (convertValue a2) (convertExpression a3) - Just "UNCHANGED" -> case as of - Just [a] -> liftA H.Unchanged (manyIdentifiers a) - Just "AND" -> case as of - Just es -> fmap H.ActionAnd (mapM convertExpression es) - Just "EQ" -> case as of - Just [a1, a2] -> liftA2 H.Primed (primed a1) (convertValue a2) - Just op -> Left("Unknown action operator " ++ op) - _ -> Left("Unknown action kind " ++ k) +convertAction (OperEx o as) = let r = case o of + "EXISTS3" -> case as of + [a1, a2, a3] -> liftA3 H.Exists (identifier a1) (convertValue a2) (convertExpression a3) + "FORALL3" -> case as of + [a1, a2, a3] -> liftA3 H.ForAll (identifier a1) (convertValue a2) (convertExpression a3) + "UNCHANGED" -> case as of + [a] -> liftA H.Unchanged (manyIdentifiers a) + "AND" -> case as of + es -> fmap H.ActionAnd (mapM convertExpression es) + "EQ" -> case as of + [a1, a2] -> liftA2 H.Primed (primed a1) (convertValue a2) + op -> Left("Unknown action operator " ++ op ++ " with args " ++ show as) + in left (\s -> s ++ "\nwhen converting " ++ show (OperEx o as)) r convertExpression :: Expression -> Either String H.Action -convertExpression (Expression k o as i v) = case k of - "OperEx" -> case o of - Just x -> if isValue (Expression k o as i v) then - convertValue (Expression k o as i v) >>= \x -> Right(H.Value x) - else if isPredicate (Expression k o as i v) then - convertPredicate (Expression k o as i v) >>= \x -> Right(H.Condition x) - else convertAction (Expression k o as i v) - Nothing -> Left "Operator required" - "ValEx" -> convertValue (Expression k o as i v) >>= \cv -> Right(H.Value cv) - _ -> Left ("Unknown expresion type: " ++ k) +convertExpression (OperEx o as) = if isPredicate (OperEx o as) then convertValue (OperEx o as) >>= \x -> Right(H.Condition x) else convertAction (OperEx o as) +convertExpression (ValEx v) = convertValue (ValEx v) >>= \cv -> Right(H.Condition cv) actionOperators :: [String] actionOperators = ["PRIME", "UNCHANGED"] -isValue :: Expression -> Bool -isValue (Expression k o as i v) = case o of - Just x -> if x `elem` valueOperators || any (flip isPrefixOf x) valuePrefixes - then case as of - Just es -> all isValue es - Nothing -> True - else False - Nothing -> True +temporalOperators :: [String] +temporalOperators = ["GLOBALLY", "STUTTER", "IMPLIES", "LEADS_TO"] isPredicate :: Expression -> Bool -isPredicate (Expression k o as i v) = case o of - Just x -> if x `elem` actionOperators - then False - else case as of - Just es -> all isPredicate es - Nothing -> True - Nothing -> True +isPredicate (OperEx o as) = o `notElem` actionOperators && all isPredicate as +isPredicate _ = True + +isTemporal :: Expression -> Bool +isTemporal (OperEx o as) = o `elem` temporalOperators || any isTemporal as +isTemporal _ = False convertRecordValues :: [Expression] -> Either String [(H.Key, H.Value)] convertRecordValues [] = Right [] -convertRecordValues (k:v:vs) = do k <- identifierFromString k - e <- convertValue v - rs <- convertRecordValues vs - return ((H.Key k, e):rs) +convertRecordValues (ValEx l:v:vs) = do e <- convertValue v + rs <- convertRecordValues vs + return ((H.Key (val l), e):rs) parseJson :: FilePath -> IO (Either String (H.Module, [H.Definition])) parseJson file = do content <- B.readFile file diff --git a/Math.hs b/Math.hs index c462bf4..040ea08 100644 --- a/Math.hs +++ b/Math.hs @@ -54,4 +54,4 @@ number = do digits <- P.many1 P.digit let n = foldl (\x d -> 10*x + toInteger (digitToInt d)) 0 digits ws - return (Num n) + return (Lit (Num n)) diff --git a/Parser.hs b/Parser.hs index eaa7b6e..c0c2d38 100644 --- a/Parser.hs +++ b/Parser.hs @@ -141,7 +141,7 @@ action = do string "IF" string "ELSE" ws af <- action - return (If p at af) + return (ActionIf p at af) <|> do {p <- predicate; return (Condition p)} <|> @@ -282,7 +282,7 @@ mapping = do try $ do ws ws v <- value ws - return (Key i, v) + return (Key (Str i), v) primed = do try $ do i <- identifier char '\'' @@ -376,6 +376,6 @@ record = do try $ do char '[' ws return (Except i [(Ref k, v)]) -literal = do try $ do {char '\"'; cs <- many1 (noneOf reserved); char '\"'; ws; return (Str cs)} +literal = do try $ do {char '\"'; cs <- many1 (noneOf reserved); char '\"'; ws; return (Lit (Str cs))} arithmeticExpression = Math.build diff --git a/tla_specifications/ewd840/APAEWD840.json b/tla_specifications/ewd840/APAEWD840.json new file mode 100644 index 0000000..5423a5f --- /dev/null +++ b/tla_specifications/ewd840/APAEWD840.json @@ -0,0 +1,7257 @@ +{ + "name": "ApalacheIR", + "version": "1.0", + "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + "modules": [ + { + "kind": "TlaModule", + "name": "APAEWD840", + "declarations": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 12, + "column": 5 + }, + "to": { + "line": 12, + "column": 5 + } + }, + "type": "Untyped", + "kind": "TlaConstDecl", + "name": "N" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 27, + "column": 5 + }, + "to": { + "line": 27, + "column": 8 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 23, + "column": 5 + }, + "to": { + "line": 23, + "column": 10 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 29, + "column": 5 + }, + "to": { + "line": 29, + "column": 10 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 25, + "column": 5 + }, + "to": { + "line": 25, + "column": 9 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 14, + "column": 1 + }, + "to": { + "line": 14, + "column": 10 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "MaxN", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 14, + "column": 9 + }, + "to": { + "line": 14, + "column": 10 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 20 + } + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 32, + "column": 1 + }, + "to": { + "line": 32, + "column": 27 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Color", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 32, + "column": 10 + }, + "to": { + "line": 32, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 32, + "column": 11 + }, + "to": { + "line": 32, + "column": 17 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 32, + "column": 20 + }, + "to": { + "line": 32, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 15, + "column": 1 + }, + "to": { + "line": 15, + "column": 23 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "ConstInit4", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 15, + "column": 15 + }, + "to": { + "line": 15, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_IN", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 15, + "column": 15 + }, + "to": { + "line": 15, + "column": 15 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "N" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 15, + "column": 21 + }, + "to": { + "line": 15, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 15, + "column": 22 + }, + "to": { + "line": 15, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 4 + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 16, + "column": 1 + }, + "to": { + "line": 16, + "column": 25 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "ConstInit10", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 16, + "column": 16 + }, + "to": { + "line": 16, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_IN", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 16, + "column": 16 + }, + "to": { + "line": 16, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "N" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 16, + "column": 22 + }, + "to": { + "line": 16, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 16, + "column": 23 + }, + "to": { + "line": 16, + "column": 24 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 10 + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 17, + "column": 1 + }, + "to": { + "line": 17, + "column": 29 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "ConstInitAll20", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 17, + "column": 19 + }, + "to": { + "line": 17, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_IN", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 17, + "column": 19 + }, + "to": { + "line": 17, + "column": 19 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "N" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 17, + "column": 25 + }, + "to": { + "line": 17, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "INT_RANGE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 17, + "column": 25 + }, + "to": { + "line": 17, + "column": 25 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 2 + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 17, + "column": 28 + }, + "to": { + "line": 17, + "column": 29 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 50 + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 1 + }, + "to": { + "line": 31, + "column": 33 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Nodes", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 10 + }, + "to": { + "line": 31, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_FILTER", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 10 + }, + "to": { + "line": 31, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 17 + }, + "to": { + "line": 31, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "INT_RANGE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 17 + }, + "to": { + "line": 31, + "column": 17 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 20 + }, + "to": { + "line": 31, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 20 + }, + "to": { + "line": 31, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "MaxN" + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 27 + }, + "to": { + "line": 31, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 27 + }, + "to": { + "line": 31, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 31, + "column": 31 + }, + "to": { + "line": 31, + "column": 31 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "N" + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 55, + "column": 1 + }, + "to": { + "line": 61, + "column": 43 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "InitiateProbe", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 56, + "column": 3 + }, + "to": { + "line": 61, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 56, + "column": 6 + }, + "to": { + "line": 56, + "column": 13 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 56, + "column": 6 + }, + "to": { + "line": 56, + "column": 9 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 56, + "column": 13 + }, + "to": { + "line": 56, + "column": 13 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 6 + }, + "to": { + "line": 57, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 6 + }, + "to": { + "line": 57, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 6 + }, + "to": { + "line": 57, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 15 + }, + "to": { + "line": 57, + "column": 21 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 26 + }, + "to": { + "line": 57, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 26 + }, + "to": { + "line": 57, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 26 + }, + "to": { + "line": 57, + "column": 30 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 32 + }, + "to": { + "line": 57, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 57, + "column": 37 + }, + "to": { + "line": 57, + "column": 43 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 58, + "column": 6 + }, + "to": { + "line": 58, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 58, + "column": 6 + }, + "to": { + "line": 58, + "column": 10 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 58, + "column": 6 + }, + "to": { + "line": 58, + "column": 9 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 58, + "column": 14 + }, + "to": { + "line": 58, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "MINUS", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 58, + "column": 14 + }, + "to": { + "line": 58, + "column": 14 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "N" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 58, + "column": 16 + }, + "to": { + "line": 58, + "column": 16 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 1 + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 59, + "column": 6 + }, + "to": { + "line": 59, + "column": 22 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 59, + "column": 6 + }, + "to": { + "line": 59, + "column": 12 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 59, + "column": 6 + }, + "to": { + "line": 59, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 59, + "column": 16 + }, + "to": { + "line": 59, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 60, + "column": 6 + }, + "to": { + "line": 60, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 60, + "column": 6 + }, + "to": { + "line": 60, + "column": 12 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 60, + "column": 6 + }, + "to": { + "line": 60, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 60, + "column": 16 + }, + "to": { + "line": 60, + "column": 21 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 6 + }, + "to": { + "line": 61, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 6 + }, + "to": { + "line": 61, + "column": 11 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 6 + }, + "to": { + "line": 61, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 15 + }, + "to": { + "line": 61, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 16 + }, + "to": { + "line": 61, + "column": 20 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 29 + }, + "to": { + "line": 61, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 31 + }, + "to": { + "line": 61, + "column": 31 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 61, + "column": 36 + }, + "to": { + "line": 61, + "column": 42 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 73, + "column": 1 + }, + "to": { + "line": 79, + "column": 43 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "PassToken", + "formalParams": [ + { + "kind": "OperParam", + "name": "i", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 74, + "column": 3 + }, + "to": { + "line": 79, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 74, + "column": 6 + }, + "to": { + "line": 74, + "column": 13 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 74, + "column": 6 + }, + "to": { + "line": 74, + "column": 9 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 74, + "column": 13 + }, + "to": { + "line": 74, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 6 + }, + "to": { + "line": 75, + "column": 58 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 6 + }, + "to": { + "line": 75, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 6 + }, + "to": { + "line": 75, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 8 + }, + "to": { + "line": 75, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 8 + }, + "to": { + "line": 75, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 15 + }, + "to": { + "line": 75, + "column": 15 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 21 + }, + "to": { + "line": 75, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 21 + }, + "to": { + "line": 75, + "column": 28 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 21 + }, + "to": { + "line": 75, + "column": 25 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 27 + }, + "to": { + "line": 75, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 32 + }, + "to": { + "line": 75, + "column": 38 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 43 + }, + "to": { + "line": 75, + "column": 58 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 43 + }, + "to": { + "line": 75, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 75, + "column": 52 + }, + "to": { + "line": 75, + "column": 58 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 76, + "column": 6 + }, + "to": { + "line": 76, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 76, + "column": 6 + }, + "to": { + "line": 76, + "column": 10 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 76, + "column": 6 + }, + "to": { + "line": 76, + "column": 9 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 76, + "column": 14 + }, + "to": { + "line": 76, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "MINUS", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 76, + "column": 14 + }, + "to": { + "line": 76, + "column": 14 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 76, + "column": 16 + }, + "to": { + "line": 76, + "column": 16 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 1 + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 6 + }, + "to": { + "line": 77, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 6 + }, + "to": { + "line": 77, + "column": 12 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 6 + }, + "to": { + "line": 77, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 16 + }, + "to": { + "line": 77, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IF_THEN_ELSE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 19 + }, + "to": { + "line": 77, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 19 + }, + "to": { + "line": 77, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 19 + }, + "to": { + "line": 77, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 25 + }, + "to": { + "line": 77, + "column": 25 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 30 + }, + "to": { + "line": 77, + "column": 36 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 43 + }, + "to": { + "line": 77, + "column": 49 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 77, + "column": 56 + }, + "to": { + "line": 77, + "column": 61 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 78, + "column": 6 + }, + "to": { + "line": 78, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 78, + "column": 6 + }, + "to": { + "line": 78, + "column": 12 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 78, + "column": 6 + }, + "to": { + "line": 78, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 78, + "column": 16 + }, + "to": { + "line": 78, + "column": 21 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 6 + }, + "to": { + "line": 79, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 6 + }, + "to": { + "line": 79, + "column": 11 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 6 + }, + "to": { + "line": 79, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 15 + }, + "to": { + "line": 79, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 16 + }, + "to": { + "line": 79, + "column": 20 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 29 + }, + "to": { + "line": 79, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 31 + }, + "to": { + "line": 79, + "column": 31 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 79, + "column": 36 + }, + "to": { + "line": 79, + "column": 42 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 101, + "column": 1 + }, + "to": { + "line": 104, + "column": 38 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Deactivate", + "formalParams": [ + { + "kind": "OperParam", + "name": "i", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 102, + "column": 3 + }, + "to": { + "line": 104, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 102, + "column": 6 + }, + "to": { + "line": 102, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 102, + "column": 6 + }, + "to": { + "line": 102, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 102, + "column": 13 + }, + "to": { + "line": 102, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 6 + }, + "to": { + "line": 103, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 6 + }, + "to": { + "line": 103, + "column": 12 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 6 + }, + "to": { + "line": 103, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 16 + }, + "to": { + "line": 103, + "column": 43 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 17 + }, + "to": { + "line": 103, + "column": 22 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 31 + }, + "to": { + "line": 103, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 33 + }, + "to": { + "line": 103, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 103, + "column": 38 + }, + "to": { + "line": 103, + "column": 42 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 104, + "column": 6 + }, + "to": { + "line": 104, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 104, + "column": 16 + }, + "to": { + "line": 104, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 104, + "column": 18 + }, + "to": { + "line": 104, + "column": 22 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 104, + "column": 25 + }, + "to": { + "line": 104, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 104, + "column": 31 + }, + "to": { + "line": 104, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 116, + "column": 1 + }, + "to": { + "line": 116, + "column": 39 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "vars", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 116, + "column": 9 + }, + "to": { + "line": 116, + "column": 39 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 116, + "column": 11 + }, + "to": { + "line": 116, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 116, + "column": 19 + }, + "to": { + "line": 116, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 116, + "column": 26 + }, + "to": { + "line": 116, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 116, + "column": 32 + }, + "to": { + "line": 116, + "column": 37 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 125, + "column": 1 + }, + "to": { + "line": 125, + "column": 36 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "TokenAlwaysBlack", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 125, + "column": 21 + }, + "to": { + "line": 125, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 125, + "column": 21 + }, + "to": { + "line": 125, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 125, + "column": 30 + }, + "to": { + "line": 125, + "column": 36 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 133, + "column": 1 + }, + "to": { + "line": 135, + "column": 38 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "terminationDetected", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 3 + }, + "to": { + "line": 135, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 6 + }, + "to": { + "line": 134, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 6 + }, + "to": { + "line": 134, + "column": 13 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 6 + }, + "to": { + "line": 134, + "column": 9 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 13 + }, + "to": { + "line": 134, + "column": 13 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 18 + }, + "to": { + "line": 134, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 18 + }, + "to": { + "line": 134, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 134, + "column": 27 + }, + "to": { + "line": 134, + "column": 33 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 6 + }, + "to": { + "line": 135, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 6 + }, + "to": { + "line": 135, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 6 + }, + "to": { + "line": 135, + "column": 13 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 6 + }, + "to": { + "line": 135, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 12 + }, + "to": { + "line": 135, + "column": 12 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 17 + }, + "to": { + "line": 135, + "column": 23 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 28 + }, + "to": { + "line": 135, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 30 + }, + "to": { + "line": 135, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 30 + }, + "to": { + "line": 135, + "column": 35 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 135, + "column": 37 + }, + "to": { + "line": 135, + "column": 37 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 44, + "column": 1 + }, + "to": { + "line": 48, + "column": 21 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Init", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 3 + }, + "to": { + "line": 48, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 6 + }, + "to": { + "line": 45, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 6 + }, + "to": { + "line": 45, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 15 + }, + "to": { + "line": 45, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_CTOR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 32 + }, + "to": { + "line": 45, + "column": 35 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": true + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 15 + }, + "to": { + "line": 45, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "n" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 22 + }, + "to": { + "line": 45, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 45, + "column": 22 + }, + "to": { + "line": 45, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 6 + }, + "to": { + "line": 46, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 6 + }, + "to": { + "line": 46, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 14 + }, + "to": { + "line": 46, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_CTOR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 31 + }, + "to": { + "line": 46, + "column": 37 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "white" + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 14 + }, + "to": { + "line": 46, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "n" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 21 + }, + "to": { + "line": 46, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 46, + "column": 21 + }, + "to": { + "line": 46, + "column": 25 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 47, + "column": 6 + }, + "to": { + "line": 47, + "column": 13 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 47, + "column": 6 + }, + "to": { + "line": 47, + "column": 9 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 47, + "column": 13 + }, + "to": { + "line": 47, + "column": 13 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 48, + "column": 6 + }, + "to": { + "line": 48, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 48, + "column": 6 + }, + "to": { + "line": 48, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 48, + "column": 15 + }, + "to": { + "line": 48, + "column": 21 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 1 + }, + "to": { + "line": 84, + "column": 62 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "System", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 11 + }, + "to": { + "line": 84, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 11 + }, + "to": { + "line": 84, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 11 + }, + "to": { + "line": 84, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "InitiateProbe" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 28 + }, + "to": { + "line": 84, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 28 + }, + "to": { + "line": 84, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 37 + }, + "to": { + "line": 84, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_MINUS", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 37 + }, + "to": { + "line": 84, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 37 + }, + "to": { + "line": 84, + "column": 41 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 45 + }, + "to": { + "line": 84, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 46 + }, + "to": { + "line": 84, + "column": 46 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 51 + }, + "to": { + "line": 84, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 51 + }, + "to": { + "line": 84, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "PassToken" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 84, + "column": 61 + }, + "to": { + "line": 84, + "column": 61 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 91, + "column": 1 + }, + "to": { + "line": 96, + "column": 31 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "SendMsg", + "formalParams": [ + { + "kind": "OperParam", + "name": "i", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 92, + "column": 3 + }, + "to": { + "line": 96, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 92, + "column": 6 + }, + "to": { + "line": 92, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 92, + "column": 6 + }, + "to": { + "line": 92, + "column": 11 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 92, + "column": 13 + }, + "to": { + "line": 92, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 6 + }, + "to": { + "line": 95, + "column": 68 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 6 + }, + "to": { + "line": 95, + "column": 68 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 15 + }, + "to": { + "line": 93, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_MINUS", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 15 + }, + "to": { + "line": 93, + "column": 19 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 15 + }, + "to": { + "line": 93, + "column": 19 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 23 + }, + "to": { + "line": 93, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 93, + "column": 24 + }, + "to": { + "line": 93, + "column": 24 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 9 + }, + "to": { + "line": 95, + "column": 68 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 12 + }, + "to": { + "line": 94, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 12 + }, + "to": { + "line": 94, + "column": 18 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 12 + }, + "to": { + "line": 94, + "column": 17 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 22 + }, + "to": { + "line": 94, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 23 + }, + "to": { + "line": 94, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 37 + }, + "to": { + "line": 94, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 39 + }, + "to": { + "line": 94, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 94, + "column": 44 + }, + "to": { + "line": 94, + "column": 47 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": true + } + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 12 + }, + "to": { + "line": 95, + "column": 68 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 12 + }, + "to": { + "line": 95, + "column": 17 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 12 + }, + "to": { + "line": 95, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 21 + }, + "to": { + "line": 95, + "column": 68 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 22 + }, + "to": { + "line": 95, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 35 + }, + "to": { + "line": 95, + "column": 67 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 37 + }, + "to": { + "line": 95, + "column": 37 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 42 + }, + "to": { + "line": 95, + "column": 67 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IF_THEN_ELSE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 45 + }, + "to": { + "line": 95, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 45 + }, + "to": { + "line": 95, + "column": 45 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 47 + }, + "to": { + "line": 95, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 54 + }, + "to": { + "line": 95, + "column": 60 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 35 + }, + "to": { + "line": 95, + "column": 67 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 22 + }, + "to": { + "line": 95, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 95, + "column": 37 + }, + "to": { + "line": 95, + "column": 37 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 96, + "column": 6 + }, + "to": { + "line": 96, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 96, + "column": 16 + }, + "to": { + "line": 96, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 96, + "column": 18 + }, + "to": { + "line": 96, + "column": 21 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 96, + "column": 24 + }, + "to": { + "line": 96, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 1 + }, + "to": { + "line": 127, + "column": 46 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "NeverChangeColor", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 21 + }, + "to": { + "line": 127, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GLOBALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 23 + }, + "to": { + "line": 127, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "STUTTER", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 25 + }, + "to": { + "line": 127, + "column": 39 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 35 + }, + "to": { + "line": 127, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 43 + }, + "to": { + "line": 127, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 127, + "column": 43 + }, + "to": { + "line": 127, + "column": 46 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 137, + "column": 1 + }, + "to": { + "line": 138, + "column": 53 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "TerminationDetection", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 3 + }, + "to": { + "line": 138, + "column": 53 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IMPLIES", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 3 + }, + "to": { + "line": 138, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 3 + }, + "to": { + "line": 138, + "column": 21 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "terminationDetected" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 26 + }, + "to": { + "line": 138, + "column": 53 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FORALL3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 26 + }, + "to": { + "line": 138, + "column": 53 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 35 + }, + "to": { + "line": 138, + "column": 39 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 35 + }, + "to": { + "line": 138, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 43 + }, + "to": { + "line": 138, + "column": 53 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 45 + }, + "to": { + "line": 138, + "column": 53 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 45 + }, + "to": { + "line": 138, + "column": 50 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 138, + "column": 52 + }, + "to": { + "line": 138, + "column": 52 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 143, + "column": 1 + }, + "to": { + "line": 144, + "column": 55 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Liveness", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 3 + }, + "to": { + "line": 144, + "column": 55 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LEADS_TO", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 4 + }, + "to": { + "line": 144, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FORALL3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 4 + }, + "to": { + "line": 144, + "column": 31 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 13 + }, + "to": { + "line": 144, + "column": 17 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 13 + }, + "to": { + "line": 144, + "column": 17 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 21 + }, + "to": { + "line": 144, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 23 + }, + "to": { + "line": 144, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 23 + }, + "to": { + "line": 144, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 30 + }, + "to": { + "line": 144, + "column": 30 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 37 + }, + "to": { + "line": 144, + "column": 55 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 144, + "column": 37 + }, + "to": { + "line": 144, + "column": 55 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "terminationDetected" + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 151, + "column": 1 + }, + "to": { + "line": 152, + "column": 60 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "FalseLiveness", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 3 + }, + "to": { + "line": 152, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LEADS_TO", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 4 + }, + "to": { + "line": 152, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FORALL3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 4 + }, + "to": { + "line": 152, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 13 + }, + "to": { + "line": 152, + "column": 17 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 13 + }, + "to": { + "line": 152, + "column": 17 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 21 + }, + "to": { + "line": 152, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GLOBALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 23 + }, + "to": { + "line": 152, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EVENTUALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 26 + }, + "to": { + "line": 152, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 28 + }, + "to": { + "line": 152, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 28 + }, + "to": { + "line": 152, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 35 + }, + "to": { + "line": 152, + "column": 35 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 42 + }, + "to": { + "line": 152, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 152, + "column": 42 + }, + "to": { + "line": 152, + "column": 60 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "terminationDetected" + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 170, + "column": 1 + }, + "to": { + "line": 173, + "column": 26 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Inv", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 3 + }, + "to": { + "line": 173, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 6 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LABEL", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 11 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FORALL3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 11 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 20 + }, + "to": { + "line": 171, + "column": 24 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 20 + }, + "to": { + "line": 171, + "column": 24 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 28 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IMPLIES", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 28 + }, + "to": { + "line": 171, + "column": 35 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 28 + }, + "to": { + "line": 171, + "column": 31 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 35 + }, + "to": { + "line": 171, + "column": 35 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 40 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 42 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 42 + }, + "to": { + "line": 171, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 49 + }, + "to": { + "line": 171, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 171, + "column": 6 + }, + "to": { + "line": 171, + "column": 50 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "P0" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 6 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LABEL", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 11 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 11 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 20 + }, + "to": { + "line": 172, + "column": 24 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 20 + }, + "to": { + "line": 172, + "column": 24 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 27 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IMPLIES", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 28 + }, + "to": { + "line": 172, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 28 + }, + "to": { + "line": 172, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 28 + }, + "to": { + "line": 172, + "column": 28 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 33 + }, + "to": { + "line": 172, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 38 + }, + "to": { + "line": 172, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LE", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 38 + }, + "to": { + "line": 172, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 43 + }, + "to": { + "line": 172, + "column": 46 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tpos" + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 52 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 52 + }, + "to": { + "line": 172, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 52 + }, + "to": { + "line": 172, + "column": 56 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "color" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 58 + }, + "to": { + "line": 172, + "column": 58 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "j" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 63 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 172, + "column": 6 + }, + "to": { + "line": 172, + "column": 69 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "P1" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 173, + "column": 6 + }, + "to": { + "line": 173, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LABEL", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 173, + "column": 11 + }, + "to": { + "line": 173, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 173, + "column": 11 + }, + "to": { + "line": 173, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tcolor" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 173, + "column": 20 + }, + "to": { + "line": 173, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "black" + } + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 173, + "column": 6 + }, + "to": { + "line": 173, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "P2" + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 1 + }, + "to": { + "line": 109, + "column": 59 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Environment", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 16 + }, + "to": { + "line": 109, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 16 + }, + "to": { + "line": 109, + "column": 59 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 25 + }, + "to": { + "line": 109, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 25 + }, + "to": { + "line": 109, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 33 + }, + "to": { + "line": 109, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 33 + }, + "to": { + "line": 109, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 33 + }, + "to": { + "line": 109, + "column": 42 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "SendMsg" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 41 + }, + "to": { + "line": 109, + "column": 41 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 47 + }, + "to": { + "line": 109, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 47 + }, + "to": { + "line": 109, + "column": 59 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Deactivate" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 109, + "column": 58 + }, + "to": { + "line": 109, + "column": 58 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 164, + "column": 1 + }, + "to": { + "line": 165, + "column": 78 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "AllNodesTerminateIfNoMessages", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 3 + }, + "to": { + "line": 165, + "column": 78 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IMPLIES", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 3 + }, + "to": { + "line": 165, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EVENTUALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 5 + }, + "to": { + "line": 165, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GLOBALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 7 + }, + "to": { + "line": 165, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "STUTTER", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 8 + }, + "to": { + "line": 165, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FORALL3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 8 + }, + "to": { + "line": 165, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 17 + }, + "to": { + "line": 165, + "column": 21 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 17 + }, + "to": { + "line": 165, + "column": 21 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 25 + }, + "to": { + "line": 165, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 27 + }, + "to": { + "line": 165, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 27 + }, + "to": { + "line": 165, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "SendMsg" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 35 + }, + "to": { + "line": 165, + "column": 35 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 39 + }, + "to": { + "line": 165, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 39 + }, + "to": { + "line": 165, + "column": 42 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 47 + }, + "to": { + "line": 165, + "column": 78 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EVENTUALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 50 + }, + "to": { + "line": 165, + "column": 77 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FORALL3", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 50 + }, + "to": { + "line": 165, + "column": 77 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 59 + }, + "to": { + "line": 165, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 59 + }, + "to": { + "line": 165, + "column": 63 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Nodes" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 67 + }, + "to": { + "line": 165, + "column": 77 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "NOT", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 69 + }, + "to": { + "line": 165, + "column": 77 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 69 + }, + "to": { + "line": 165, + "column": 74 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "active" + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 165, + "column": 76 + }, + "to": { + "line": 165, + "column": 76 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "i" + } + ] + } + ] + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 114, + "column": 1 + }, + "to": { + "line": 114, + "column": 29 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Next", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 114, + "column": 9 + }, + "to": { + "line": 114, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 114, + "column": 9 + }, + "to": { + "line": 114, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 114, + "column": 9 + }, + "to": { + "line": 114, + "column": 14 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "System" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 114, + "column": 19 + }, + "to": { + "line": 114, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 114, + "column": 19 + }, + "to": { + "line": 114, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Environment" + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 1 + }, + "to": { + "line": 118, + "column": 48 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Spec", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 9 + }, + "to": { + "line": 118, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 9 + }, + "to": { + "line": 118, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 9 + }, + "to": { + "line": 118, + "column": 12 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 9 + }, + "to": { + "line": 118, + "column": 12 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Init" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 17 + }, + "to": { + "line": 118, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GLOBALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 19 + }, + "to": { + "line": 118, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "STUTTER", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 20 + }, + "to": { + "line": 118, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 20 + }, + "to": { + "line": 118, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Next" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 26 + }, + "to": { + "line": 118, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 26 + }, + "to": { + "line": 118, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 34 + }, + "to": { + "line": 118, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "WEAK_FAIRNESS", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 37 + }, + "to": { + "line": 118, + "column": 40 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 37 + }, + "to": { + "line": 118, + "column": 40 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 42 + }, + "to": { + "line": 118, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 118, + "column": 42 + }, + "to": { + "line": 118, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "System" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 1 + }, + "to": { + "line": 163, + "column": 52 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "SpecWFNext", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 15 + }, + "to": { + "line": 163, + "column": 52 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 15 + }, + "to": { + "line": 163, + "column": 35 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 15 + }, + "to": { + "line": 163, + "column": 18 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 15 + }, + "to": { + "line": 163, + "column": 18 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Init" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 23 + }, + "to": { + "line": 163, + "column": 35 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GLOBALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 25 + }, + "to": { + "line": 163, + "column": 35 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "STUTTER", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 26 + }, + "to": { + "line": 163, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 26 + }, + "to": { + "line": 163, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Next" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 32 + }, + "to": { + "line": 163, + "column": 35 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 32 + }, + "to": { + "line": 163, + "column": 35 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 40 + }, + "to": { + "line": 163, + "column": 52 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "WEAK_FAIRNESS", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 43 + }, + "to": { + "line": 163, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 43 + }, + "to": { + "line": 163, + "column": 46 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 48 + }, + "to": { + "line": 163, + "column": 51 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 163, + "column": 48 + }, + "to": { + "line": 163, + "column": 51 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Next" + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 1 + }, + "to": { + "line": 185, + "column": 42 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "CheckInductiveSpec", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 23 + }, + "to": { + "line": 185, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 23 + }, + "to": { + "line": 185, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 23 + }, + "to": { + "line": 185, + "column": 25 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Inv" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 30 + }, + "to": { + "line": 185, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GLOBALLY", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 32 + }, + "to": { + "line": 185, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "STUTTER", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 33 + }, + "to": { + "line": 185, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 33 + }, + "to": { + "line": 185, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "Next" + } + ] + }, + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 39 + }, + "to": { + "line": 185, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "APAEWD840", + "from": { + "line": 185, + "column": 39 + }, + "to": { + "line": 185, + "column": 42 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "vars" + } + ] + } + ] + } + ] + } + ] + } + } + ] + } + ] +} \ No newline at end of file diff --git a/tla_specifications/ewd840/APAEWD840.tla b/tla_specifications/ewd840/APAEWD840.tla new file mode 100644 index 0000000..6ee672c --- /dev/null +++ b/tla_specifications/ewd840/APAEWD840.tla @@ -0,0 +1,190 @@ +------------------------------- MODULE APAEWD840 ------------------------------- +(***************************************************************************) +(* TLA+ specification of an algorithm for distributed termination *) +(* detection on a ring, due to Dijkstra, published as EWD 840: *) +(* Derivation of a termination detection algorithm for distributed *) +(* computations (with W.H.J.Feijen and A.J.M. van Gasteren). *) +(***************************************************************************) +EXTENDS Naturals + +CONSTANT + \* @type: Int; + N + +MaxN == 20 +ConstInit4 == N \in {4} +ConstInit10 == N \in {10} +ConstInitAll20 == N \in 2..50 + +(*ASSUME NAssumption == N \in Nat \ {0}*) + +VARIABLES + \* @type: Int -> Bool; + active, + \* @type: Int -> Str; + color, + \* @type: Int; + tpos, + \* @type: Str; + tcolor + +Nodes == {i \in 0..MaxN : i < N } \* 0 .. N-1 +Color == {"white", "black"} + +\* TypeOK == +\* /\ active \in [Nodes -> BOOLEAN] \* status of nodes (active or passive) +\* /\ color \in [Nodes -> Color] \* color of nodes +\* /\ tpos \in Nodes \* token position +\* /\ tcolor \in Color \* token color + +(***************************************************************************) +(* Initially the token is black. The other variables may take any *) +(* "type-correct" values. *) +(***************************************************************************) +Init == + /\ active = [n \in Nodes |-> TRUE] + /\ color = [n \in Nodes |-> "white"] + /\ tpos = 0 + /\ tcolor = "black" + +(***************************************************************************) +(* Node 0 may initiate a probe when it has the token and when either it is *) +(* black or the token is black. It passes a white token to node N-1 and *) +(* paints itself white. *) +(***************************************************************************) +InitiateProbe == + /\ tpos = 0 + /\ tcolor = "black" \/ color[0] = "black" + /\ tpos' = N-1 + /\ tcolor' = "white" + /\ active' = active + /\ color' = [color EXCEPT ![0] = "white"] + +(***************************************************************************) +(* A node i different from 0 that possesses the token may pass it to node *) +(* i-1 under the following circumstances: *) +(* - node i is inactive or *) +(* - node i is colored black or *) +(* - the token is black. *) +(* Note that the last two conditions will result in an inconclusive round, *) +(* since the token will be black. The token will be stained if node i is *) +(* black, otherwise its color is unchanged. Node i will be made white. *) +(***************************************************************************) +PassToken(i) == + /\ tpos = i + /\ ~ active[i] \/ color[i] = "black" \/ tcolor = "black" + /\ tpos' = i-1 + /\ tcolor' = IF color[i] = "black" THEN "black" ELSE tcolor + /\ active' = active + /\ color' = [color EXCEPT ![i] = "white"] + +(***************************************************************************) +(* token passing actions controlled by the termination detection algorithm *) +(***************************************************************************) +System == InitiateProbe \/ \E i \in Nodes \ {0} : PassToken(i) + +(***************************************************************************) +(* An active node i may activate another node j by sending it a message. *) +(* If j>i (hence activation goes against the direction of the token being *) +(* passed), then node i becomes black. *) +(***************************************************************************) +SendMsg(i) == + /\ active[i] + /\ \E j \in Nodes \ {i} : + /\ active' = [active EXCEPT ![j] = TRUE] + /\ color' = [color EXCEPT ![i] = IF j>i THEN "black" ELSE @] + /\ UNCHANGED <> + +(***************************************************************************) +(* Any active node may become inactive at any moment. *) +(***************************************************************************) +Deactivate(i) == + /\ active[i] + /\ active' = [active EXCEPT ![i] = FALSE] + /\ UNCHANGED <> + +(***************************************************************************) +(* actions performed by the underlying algorithm *) +(***************************************************************************) +Environment == \E i \in Nodes : SendMsg(i) \/ Deactivate(i) + +(***************************************************************************) +(* next-state relation: disjunction of above actions *) +(***************************************************************************) +Next == System \/ Environment + +vars == <> + +Spec == Init /\ [][Next]_vars /\ WF_vars(System) + +----------------------------------------------------------------------------- + +(***************************************************************************) +(* Non-properties, useful for validating the specification with TLC. *) +(***************************************************************************) +TokenAlwaysBlack == tcolor = "black" + +NeverChangeColor == [][ UNCHANGED color ]_vars + +(***************************************************************************) +(* Main safety property: if there is a white token at node 0 then every *) +(* node is inactive. *) +(***************************************************************************) +terminationDetected == + /\ tpos = 0 /\ tcolor = "white" + /\ color[0] = "white" /\ ~ active[0] + +TerminationDetection == + terminationDetected => \A i \in Nodes : ~ active[i] + +(***************************************************************************) +(* Liveness property: termination is eventually detected. *) +(***************************************************************************) +Liveness == + (\A i \in Nodes : ~ active[i]) ~> terminationDetected + +(***************************************************************************) +(* The following property asserts that when every process always *) +(* eventually terminates then eventually termination will be detected. *) +(* It does not hold since processes can wake up each other. *) +(***************************************************************************) +FalseLiveness == + (\A i \in Nodes : []<> ~ active[i]) ~> terminationDetected + +(***************************************************************************) +(* The following property says that eventually all nodes will terminate *) +(* assuming that from some point onwards no messages are sent. It is *) +(* not supposed to hold: any node may indefinitely perform local *) +(* computations. However, this property is verified if the fairness *) +(* condition WF_vars(Next) is used instead of only WF_vars(System) that *) +(* requires fairness of the actions controlled by termination detection. *) +(***************************************************************************) + +SpecWFNext == Init /\ [][Next]_vars /\ WF_vars(Next) +AllNodesTerminateIfNoMessages == + <>[][\A i \in Nodes : ~ SendMsg(i)]_vars => <>(\A i \in Nodes : ~ active[i]) + +(***************************************************************************) +(* Dijkstra's inductive invariant *) +(***************************************************************************) +Inv == + \/ P0:: \A i \in Nodes : tpos < i => ~ active[i] + \/ P1:: \E j \in Nodes: (0 <= j /\ j <= tpos) => color[j] = "black" + \/ P2:: tcolor = "black" + + (*\/ P1:: \E j \in 0 .. tpos : color[j] = "black"*) + +(* InvAndTypeOK == TypeOK /\ Inv *) + +(***************************************************************************) +(* Use the following specification to let TLC check that the predicate *) +(* TypeOK /\ Inv is inductive for EWD 840: verify that it is an *) +(* (ordinary) invariant of a specification obtained by replacing the *) +(* initial condition by that conjunction. *) +(***************************************************************************) +CheckInductiveSpec == Inv /\ [][Next]_vars +============================================================================= +\* Modification History +\* Last modified Wed Mar 20 16:57:55 CET 2019 by igor +\* Last modified Tue Jun 28 18:17:45 CEST 2016 by merz +\* Created Mon Sep 09 11:33:10 CEST 2013 by merz diff --git a/tla_specifications/ewd840/MC.cfg b/tla_specifications/ewd840/MC.cfg new file mode 100644 index 0000000..449e8c8 --- /dev/null +++ b/tla_specifications/ewd840/MC.cfg @@ -0,0 +1,9 @@ +\* CONSTANT definitions +CONSTANT +N <- MC_N +INIT +MC_Init +NEXT +Next +INVARIANT +MC_Inv diff --git a/tla_specifications/ewd840/MC10.tla b/tla_specifications/ewd840/MC10.tla new file mode 100644 index 0000000..554b8f8 --- /dev/null +++ b/tla_specifications/ewd840/MC10.tla @@ -0,0 +1,9 @@ +---- MODULE MC10 ---- +EXTENDS APAEWD840, TLC + +MC_N == 10 +MC_Init == Init +MC_Inv == Inv +============================================================================= +\* Modification History +\* Created Mon Mar 11 13:36:00 CET 2019 by igor diff --git a/tla_specifications/ewd840/MC4.tla b/tla_specifications/ewd840/MC4.tla new file mode 100644 index 0000000..eb861df --- /dev/null +++ b/tla_specifications/ewd840/MC4.tla @@ -0,0 +1,9 @@ +---- MODULE MC4 ---- +EXTENDS APAEWD840, TLC + +MC_N == 4 +MC_Init == Init +MC_Inv == Inv +============================================================================= +\* Modification History +\* Created Mon Mar 11 13:36:00 CET 2019 by igor diff --git a/tla_specifications/ewd840/MC4Inv.tla b/tla_specifications/ewd840/MC4Inv.tla new file mode 100644 index 0000000..373d609 --- /dev/null +++ b/tla_specifications/ewd840/MC4Inv.tla @@ -0,0 +1,9 @@ +---- MODULE MC4Inv ---- +EXTENDS APAEWD840, TLC + +MC_N == 4 +MC_Init == InvAndTypeOK +MC_Inv == InvAndTypeOK +============================================================================= +\* Modification History +\* Created Mon Mar 11 13:36:00 CET 2019 by igor diff --git a/tla_specifications/ewd840/README.md b/tla_specifications/ewd840/README.md new file mode 100644 index 0000000..1f4f28b --- /dev/null +++ b/tla_specifications/ewd840/README.md @@ -0,0 +1,9 @@ +# EWD840 + +Examples imported from https://github.com/informalsystems/apalache-bench/tree/trunk/performance/ewd840 + +JSON files are parsed with [Apalache](https://github.com/informalsystems/apalache): + +``` sh +apalache-mc parse --output=APAEWD840.json APAEWD840.tla +```