Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
------------------------------ MODULE imageaug ------------------------------
EXTENDS Integers, FiniteSets, TLC
CONSTANTS Documents,
Models,
MaxRetries,
NULL
ASSUME MaxRetries \in Nat \ {0}
ASSUME Cardinality(Documents) /= 0
ASSUME Cardinality(Models) /= 0
\* TODO: assumption for NULL ?
(***************************************************************************)
(* Handles batches of documents to models, where each document must be *)
(* evaluated against each model. *)
(* *)
(* Each evaluation can fail, and we must attempt to have all possible *)
(* document X model combination to be successful before returning *)
(* *)
(* We only allow a certain amount of retries to avoid infinite loops. *)
(***************************************************************************)
(*--algorithm imageaug
variables attempts = 0,
result = [d \in Documents, m \in Models |-> NULL],
todo = DOMAIN result;
define
TypeInv == /\ attempts \in 0..MaxRetries
/\ todo \in SUBSET (Documents \X Models)
/\ result \in [Documents \X Models -> {NULL, "success", "error"}]
end define;
fair process predict = "predict"
begin
Handle_Batch:
while attempts <= MaxRetries /\ Cardinality(todo) /= 0 do
Handle_Todo:
while Cardinality(todo) /= 0 do
with dm \in todo do
either result[dm] := "error";
or result[dm] := "success";
end either;
todo := todo \ {dm};
end with;
end while;
todo := {dm \in DOMAIN result: result[dm] /= "success"};
attempts := attempts + 1;
end while;
\* TODO: shouldn't this be a temporal property, <>[]... ?
\* Can't seem to get that to work though, stuttering happens.
assert \/ attempts = MaxRetries + 1
\/ \A dm \in DOMAIN result: result[dm] = "success"
end process;
end algorithm; *)
@hwayne
Copy link

hwayne commented Mar 20, 2019

Tip: if you put (**) inside a pluscal algorithm it fritzes out github's comment syntax and lets you see the TLA+ syntax in the pluscal code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment