tlaplus tlapm_alternative_parser_experiment issues

tlaplus / tlapm_alternative_parser_experiment

The rewrite of TLAPM, the TLAPS proof manager

Other

0 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Add current OCaml versions to Travis

#25 gliptak closed 5 years ago
3
Bags standard module overridden by TLAPS, exports extra declarations unrelated with bags

#24 jorgeadriano opened 6 years ago
0
Isabelle rejects a Zenon proof from `FiniteSetTheorems_proofs` if the operator `Size` is visible

#23 johnyf opened 6 years ago
0
TLAPS proves via SMT that `Len(x) \in Nat` for arbitrary x

#22 johnyf opened 6 years ago
1
placing directories of temporary files under `__tlacache__/`

#21 johnyf opened 7 years ago
0
`z3` errors due to renamed parameters: `pull-nested-quantifiers` and `mbqi`

#20 johnyf opened 7 years ago
0
veriT solver says "unknown logic AUFNIRA"

#19 johnyf opened 7 years ago
0
calling solver `veriT` on case-sensitive file systems

#18 johnyf opened 7 years ago
5
Xmlm error when module missing from include path

#17 johnyf opened 7 years ago
0
rm: cannot remove './nunchaku/tmp*.*': No such file or directory

#16 johnyf opened 7 years ago
0
DOC: list package `containers` in README

#15 johnyf opened 7 years ago
0
SMT backends CVC3 and Z3 prove `\A x: x \in BOOLEAN`

#14 johnyf opened 7 years ago
2
Add build status to README.md

#13 gliptak closed 7 years ago
0
Add .travis.yml

#12 gliptak closed 7 years ago
2
TLAPS fails to prove instances of temporal theorems

#11 muenchnerkindl opened 7 years ago
0
Wip simpler datastructures

#10 quicquid closed 7 years ago
0
Theorems from instantiated modules

#9 johnyf opened 7 years ago
0
Proofs rejected by Isabelle can go unnoticed

#8 johnyf opened 7 years ago
2
Improving support for functions of multiple arguments

#7 johnyf opened 7 years ago
0
Another case where Isabelle rejects a proof

#6 johnyf opened 7 years ago
0
Isabelle rejects a proof found by Zenon

#5 johnyf opened 7 years ago
0
Nunchaku backend does not encode tla names which are unreadable for nunchaku (e.g. intersection and numerals)

#4 quicquid opened 8 years ago
0
Tla nunchaku

#3 quicquid closed 8 years ago
0
Obligation extraction bug

#2 ML44 closed 8 years ago
2
XML Export of a Spec with only definitions creates an empty module

#1 quicquid opened 8 years ago
0

tlaplus / tlapm_alternative_parser_experiment

issues

Add current OCaml versions to Travis

Bags standard module overridden by TLAPS, exports extra declarations unrelated with bags

Isabelle rejects a Zenon proof from `FiniteSetTheorems_proofs` if the operator `Size` is visible

TLAPS proves via SMT that `Len(x) \in Nat` for arbitrary x

placing directories of temporary files under `tlacache/`

`z3` errors due to renamed parameters: `pull-nested-quantifiers` and `mbqi`

veriT solver says "unknown logic AUFNIRA"

calling solver `veriT` on case-sensitive file systems

Xmlm error when module missing from include path

rm: cannot remove './nunchaku/tmp.': No such file or directory

DOC: list package `containers` in README

SMT backends CVC3 and Z3 prove `\A x: x \in BOOLEAN`

Add build status to README.md

Add .travis.yml

TLAPS fails to prove instances of temporal theorems

Wip simpler datastructures

Theorems from instantiated modules

Proofs rejected by Isabelle can go unnoticed

Improving support for functions of multiple arguments

Another case where Isabelle rejects a proof

Isabelle rejects a proof found by Zenon

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

Tla nunchaku

Obligation extraction bug

XML Export of a Spec with only definitions creates an empty module