Silent failure when input file doesn't exist -- output suggests file exists

[lemmy]

Note the missing file extension (BlockingQueue) in the first invocation, but the message includes the extension (BlockingQueue.tla) :

Both TLC and Apalache automatically append the .tla extension if omitted.

markus@avocado:~$ tlapm BlockingQueue
(* created new ".tlacache/FiniteSets.tlaps/FiniteSets.thy" *)
(* fingerprints written in ".tlacache/FiniteSets.tlaps/fingerprints" *)
File "/usr/local/lib/tlaps/FiniteSets.tla", line 1, character 1 to line 23, character 77:
[INFO]: All 0 obligation proved.
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/usr/local/lib/tlaps/TLAPS.tla", line 1, character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
(* created new ".tlacache/BlockingQueue.tlaps/BlockingQueue.thy" *)
(* fingerprints written in ".tlacache/BlockingQueue.tlaps/fingerprints" *)
File "./BlockingQueue.tla", line 1, character 1 to line 145, character 77:
[INFO]: All 1 obligation proved.



markus@avocado:~$ tlapm BlockingQueue.tla
(* created new ".tlacache/FiniteSets.tlaps/FiniteSets.thy" *)
(* fingerprints written in ".tlacache/FiniteSets.tlaps/fingerprints" *)
File "/usr/local/lib/tlaps/FiniteSets.tla", line 1, character 1 to line 23, character 77:
[INFO]: All 0 obligation proved.
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/usr/local/lib/tlaps/TLAPS.tla", line 1, character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
(* loading fingerprints in ".tlacache/BlockingQueue.tlaps/fingerprints" *)
** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

** Unexpanded symbols: ---

(* created new ".tlacache/BlockingQueue.tlaps/BlockingQueue.thy" *)
(* fingerprints written in ".tlacache/BlockingQueue.tlaps/fingerprints" *)
File "./BlockingQueue.tla", line 127, characters 36-37:
[ERROR]: Could not prove or check:
           ASSUME NEW CONSTANT Producers,
                  NEW CONSTANT Consumers,
                  NEW CONSTANT BufCapacity,
                  Assumption ==
                    /\ Producers # {}
                    /\ Consumers # {}
                    /\ Producers \cap Consumers = {}
                    /\ BufCapacity \in Nat \ {0},
                  NEW VARIABLE buffer,
                  NEW VARIABLE waitSet,
                  vars == <<buffer, waitSet>>,
                  RunningThreads == (Producers \cup Consumers) \ waitSet,
                  NotifyOther(t) ==
                    LET S == waitSet
                    IN  IF S # {}
                          THEN \E x \in S : waitSet' = waitSet \ {x}
                          ELSE UNCHANGED waitSet,
                  Wait(t) ==
                    /\ waitSet' = waitSet \cup {t}
                    /\ UNCHANGED <<buffer>>,
                  Put(t, d) ==
                    /\ t \notin waitSet
                    /\ \/ /\ buffer < BufCapacity
                          /\ buffer' = buffer + 1
                          /\ NotifyOther(t)
                       \/ /\ buffer = BufCapacity
                          /\ Wait(t),
                  Get(t) ==
                    /\ t \notin waitSet
                    /\ \/ /\ buffer # 0
                          /\ buffer' = buffer - 1
                          /\ NotifyOther(t)
                       \/ /\ buffer = 0Silent failure when input file doesn't exist 
                          /\ Wait(t),
                  Init == /\ buffer = 0
                          /\ waitSet = {},
                  Next ==
                    \/ \E p \in Producers : Put(p, p)
                    \/ \E c \in Consumers : Get(c),
                  TypeInv ==
                    /\ buffer \in 0..BufCapacity
                    /\ waitSet \in SUBSET (Producers \cup Consumers),
                  Invariant == waitSet # Producers \cup Consumers,
                  Spec == Init /\ [][Next]_vars,
                  Assumption ,
                  IInv ==
                    /\ waitSet \in SUBSET (Producers \cup Consumers)
                    /\ Invariant
                    /\ buffer = 0 => (\E p \in Producers : p \notin waitSet)
                    /\ buffer = BufCapacity
                       => (\E c \in Consumers : c \notin waitSet)
           PROVE  IInv /\ [Next]_vars => IInv'
File "./BlockingQueue.tla", line 1, character 1 to line 145, character 77:
[ERROR]: 1/18 obligations failed.
There were backend errors processing module `"BlockingQueue"`.
 tlapm ending abnormally with Failure("backend errors: there are unproved obligations")
Raised at file "stdlib.ml", line 29, characters 17-33
Called from file "tlapm.ml", line 408, characters 12-77
Called from file "tlapm.ml", line 503, characters 23-43
Called from file "list.ml", line 121, characters 24-34
Called from file "tlapm.ml", line 506, characters 13-40
Called from file "tlapm.ml", line 518, characters 8-33

[johnyf]

Thank you for reporting this issue. This bug was caused by a comparison between the file basename, with the extension .tla added if missing, to the list of file basenames of the paths given to tlapm on the command-line.

This comparison is on the following line:

tlapm/src/proof/p_gen.ml

Line 234 in ab564e3

if not (List.mem (Filename.basename loc.Loc.file) !Params.input_files)

Adding before the above line the following lines:

let file_basename = Filename.basename loc.Loc.file in
print_string "Inside `Proof.Gen`\nFile basename:\n";
print_string (file_basename ^ "\n");
print_string "!Params.input_files:\n";
List.iter (fun x -> print_string x) !Params.input_files;
print_string "\n----";

results in the following output:

> ls nonexistent
ls: nonexistent: No such file or directory


> ls nonexistent.tla
nonexistent.tla


> cat nonexistent.tla
---- MODULE nonexistent ----

THEOREM FALSE
OBVIOUS

============================


> tlapm nonexistent
...
Inside `Proof.Gen`
File basename:
nonexistent.tla
!Params.input_files:
nonexistent
...
(* created new ".tlacache/nonexistent.tlaps/nonexistent.thy" *)
(* fingerprints written in ".tlacache/nonexistent.tlaps/fingerprints" *)
File "./nonexistent.tla", line 1, character 1 to line 6, character 28:
[INFO]: All 0 obligation proved.


> tlapm nonexistent.tla
...
Inside `Proof.Gen`
File basename:
nonexistent.tla
!Params.input_files:
nonexistent.tla
...
(* loading fingerprints in ".tlacache/nonexistent.tlaps/fingerprints" *)
** Unexpanded symbols: ---

Zenon error: exhausted search space without finding a proof
(* created new ".tlacache/nonexistent.tlaps/nonexistent.thy" *)
(* fingerprints written in ".tlacache/nonexistent.tlaps/fingerprints" *)
File "./nonexistent.tla", line 4, characters 1-7:
[ERROR]: Could not prove or check:
           FALSE
File "./nonexistent.tla", line 1, character 1 to line 6, character 28:
[ERROR]: 1/1 obligation failed.
There were backend errors processing module `"nonexistent"`.
 tlapm ending abnormally with Failure("backend errors: there are unproved obligations")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Tlapm.process_module in file "tlapm.ml", line 406, characters 12-77
Called from Tlapm.main.f in file "tlapm.ml", line 502, characters 23-43
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 505, characters 13-40
Called from Tlapm.init in file "tlapm.ml", line 517, characters 8-33

This error arises when the following condition is true:

/\ "filename" is given as an argument to `tlapm`
/\ "filename" does not end with ".tla"
/\ a file with name equal to the concatenantion of "filename" and ".tla" does exist

What tlapm does is that it first checks whether "filename" has the extension .tla. If it does, then tlapm removes it. Otherwise, tlapm keeps the filename unchanged. Next, tlapm (separately) appends the extensions .tla and .xtla, and looks for files with those filenames. If tlapm finds any such files, then it loads them (and modules mentioned in EXTENDS statements, etc).

So in both cases of invocation above, tlapm did find and load the file nonexistent.tla, which is why tlapm continued with the rest of its execution. Otherwise (had nonexistent.tla not been present), tlapm would have stopped at the phase of loading files:

> tlapm nofile
File "<unknown>":
Error: File "nofile" not found
...
 tlapm ending abnormally with Failure("Module.Parser.parse_file")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from M_save.clocking in file "m_save.ml", line 29, characters 18-22
Called from Tlapm.read_new_modules.(fun) in file "tlapm.ml", line 453, characters 8-112
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Tlapm.main in file "tlapm.ml", line 489, characters 20-43
Called from Tlapm.init in file "tlapm.ml", line 517, characters 8-33

Later, as tlapm continues its execution, it reaches the point where it decides whether to generate proof obligations for the module it is currently working on, or not.

tlapm generates proof obligations only for modules that are also inside files that were given to tlapm at the command-line. The filename stored in the location that annotates a proof is the filename that resulted after removing the extension .tla in case it was present, and adding it back again (or adding xtla, but that is not the case here). So nonexistent.tla.

The filename given on the command-line is nonexistent. tlapm checks whether "nonexistent.tla" is in the one-item list ["nonexistent"], and based on this decides to not generate any proof obligations.

One way to address this issue (assuming the .xtla-related code has been removed) is:

diff --git a/src/tlapm.ml b/src/tlapm.ml
index f46d51f..cd3bc80 100644
--- a/src/tlapm.ml
+++ b/src/tlapm.ml
@@ -470,8 +470,22 @@ let print_modules mcx =
     print_string "\nModules loaded so far:\n";
     Sm.iter (fun name mule -> Printf.printf "Module name: \"%s\"\n" name) mcx

+
+let append_ext_if_not_tla filename =
+    if Filename.check_suffix filename ".tla" then
+        filename
+    else
+        filename ^ ".tla"
+
+
+let map_paths_to_filenames paths =
+    let basenames = List.map Filename.basename paths in
+    List.map append_ext_if_not_tla basenames
+
+
 let main fs =
-  Params.input_files := List.map Filename.basename fs;
+  Params.input_files := map_paths_to_filenames fs;
+  List.iter (fun x -> print_string (x ^ "\n")) !Params.input_files;
   let () =
     List.iter begin
       fun s ->

Further comments

The code relevant to the extension .xtla is currently unused, and will likely be removed

After the code for .xtla is removed, the behavior of tlapm will be that tlapm checks whether the file ends with .tla, and if so, then tlapm removes the extension .tla. In all cases, tlapm next will append the extension .tla. The overall behavior will therefore be that tlapm appends .tla, if the given filename does not end with .tla.

(Passing a filename with two dot characters . results in a parsing error when such a file exists.)

(The value !Params.input_files that appears above is initialized at:

tlapm/src/tlapm.ml

Line 472 in ab564e3

Params.input_files := List.map Filename.basename fs;

)

[johnyf]

Addressed by commit c791f8b.