imageaug.tla

------------------------------ 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; *)

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