Improve handling of Apalache errors

[andrey-kuprianov]

Handling of errors that Modelator receives from Apalache is currently insufficient: some errors escape the regular expressions set to catch them, and result in unhandled exceptions on the Modelator side.

For example, when replacing here Int with Integer, and running modelator sample --model-path models/transfer.tla --examples Ex, I get

Sampling Ex... 
11:35:20 - /opt/homebrew/lib/python3.10/site-packages/modelator/Model.py - ERROR - Problem running apalache: 'NoneType' object is not subscriptable
Exception in thread Thread-1 (_check_sample_thread_worker):
Traceback (most recent call last):
  File "/opt/homebrew/Cellar/python@3.10/3.10.6_1/Frameworks/Python.framework/Versions/3.10/lib/python3.10/threading.py", line 1016, in _bootstrap_inner
    self.run()
  File "/opt/homebrew/Cellar/python@3.10/3.10.6_1/Frameworks/Python.framework/Versions/3.10/lib/python3.10/threading.py", line 953, in run
    self._target(*self._args, **self._kwargs)
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/Model.py", line 146, in _check_sample_thread_worker
    check_result = self._modelcheck_predicates(
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/Model.py", line 125, in _modelcheck_predicates
    raise ModelCheckingError(e)
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/utils/model_exceptions.py", line 31, in __init__
    raise exc
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/Model.py", line 117, in _modelcheck_predicates
    result = check_func(
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/checker/check.py", line 84, in check_apalache
    typecheck(tla_file_name, files)
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/typecheck.py", line 44, in typecheck
    ) = apalache_helpers.extract_typecheck_error(result["stdout"])
  File "/opt/homebrew/lib/python3.10/site-packages/modelator/utils/apalache_helpers.py", line 111, in extract_typecheck_error
    info = match_general_typing_error["info"].strip()
TypeError: 'NoneType' object is not subscriptable
Results:
- Ex ⏳
Total time: 5.06 seconds

The logic in extracting errors from Apalache should be modified to include the catch-all case, which takes care of all other cases that fall through the known ones.

[shonfeder]

would it help if we we provided structured output from apalache in the form of a Json data that indicated whether or there was any error?

[andrey-kuprianov]

@shonfeder this is a very short-term task, about the next few days only, to polish things a little before we release the Atomkraft prototype... Mid-term we will address this issue properly by integrating the Apalache server mode

[shonfeder]

I see!