---- MODULE calculator ----
EXTENDS Integers, TLC
CONSTANT NumInputs, Target

Digits == 0..9

(* --algorithm calculator
variables 
  i = 0;
  sum = 0;
define
  Invariant == sum # Target
end define;

begin
  Calculator:
    while i < NumInputs do
      with x \in Digits do
        either
          \* Add
          sum := sum + x;
        or
          \* Subtract
          sum := sum - x;
        or
          \* Multiply
          sum := sum * x;
        end either;
      end with;
      i := i + 1;
    end while;
end algorithm; *)
====