search

tlaplus / tlapm_alternative_parser_experiment

The rewrite of TLAPM, the TLAPS proof manager
Other
0 stars 0 forks source link

Nunchaku backend does not encode tla names which are unreadable for nunchaku (e.g. intersection and numerals) #4

Open quicquid opened 8 years ago

quicquid commented 8 years ago

Calling:

./tlapm test/tla/nunchaku_tests_negative.tla

Resuts in a parsing error of the backend:

Nunchaku failed with error code 1.
could not parse `./nunchaku/tmp_nun_pb_7.nun`
parse error at file './nunchaku/tmp_nun_pb_7.nun': line 4, col 8 to 9

The contents of the file is:

# Initial commands.
include "prelude.nun".
# End of initial commands.
goal ~ (1 != 2).

Remark: there should be no counter-model to this in the theory of natural numbers. But even without extending Naturals, the PM currently proves 1 # 2. The plan is to keep this behaviour in v2 of the PM.