Skip to content
This repository has been archived by the owner on May 23, 2023. It is now read-only.

Issues: tlaplus/tlapm_alternative_parser_experiment

18 Open 1 Closed
18 Open 1 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Bags standard module overridden by TLAPS, exports extra declarations unrelated with bags
#24 opened Aug 30, 2018 by jorgeadriano
Isabelle rejects a Zenon proof from FiniteSetTheorems_proofs if the operator Size is visible
#23 opened Dec 11, 2017 by johnyf
TLAPS proves via SMT that Len(x) \in Nat for arbitrary x
#22 opened Dec 10, 2017 by johnyf
1
placing directories of temporary files under __tlacache__/
#21 opened Nov 7, 2017 by johnyf
z3 errors due to renamed parameters: pull-nested-quantifiers and mbqi
#20 opened Nov 6, 2017 by johnyf
veriT solver says "unknown logic AUFNIRA"
#19 opened Nov 3, 2017 by johnyf
calling solver veriT on case-sensitive file systems
#18 opened Nov 3, 2017 by johnyf
5
Xmlm error when module missing from include path
#17 opened Oct 30, 2017 by johnyf
rm: cannot remove './nunchaku/tmp*.*': No such file or directory
#16 opened Oct 30, 2017 by johnyf
SMT backends CVC3 and Z3 prove \A x: x \in BOOLEAN
#14 opened Oct 29, 2017 by johnyf
2
TLAPS fails to prove instances of temporal theorems bug
#11 opened Sep 4, 2017 by muenchnerkindl
Theorems from instantiated modules
#9 opened Jul 19, 2017 by johnyf
Proofs rejected by Isabelle can go unnoticed
#8 opened Jul 19, 2017 by johnyf
2
Improving support for functions of multiple arguments
#7 opened Jul 19, 2017 by johnyf
Another case where Isabelle rejects a proof
#6 opened Jul 19, 2017 by johnyf
Isabelle rejects a proof found by Zenon
#5 opened Jul 19, 2017 by johnyf
Nunchaku backend does not encode tla names which are unreadable for nunchaku (e.g. intersection and numerals) bug
#4 opened Aug 8, 2016 by quicquid
XML Export of a Spec with only definitions creates an empty module bug
#1 opened Mar 31, 2016 by quicquid
ProTip! Mix and match filters to narrow down what you’re looking for.