Search results

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

Status: Open.

#24 In tlaplus/tlapm_alternative_parser_experiment;

· jorgeadriano opened on Aug 30, 2018

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

Status: Open.

#23 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Dec 11, 2017

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

Status: Open.

#22 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Dec 10, 2017

placing directories of temporary files under __tlacache__/

Status: Open.

#21 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Nov 7, 2017

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

Status: Open.

#20 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Nov 6, 2017

veriT solver says "unknown logic AUFNIRA"

Status: Open.

#19 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Nov 3, 2017

calling solver veriT on case-sensitive file systems

Status: Open.

#18 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Nov 3, 2017

Xmlm error when module missing from include path

Status: Open.

#17 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Oct 30, 2017

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

Status: Open.

#16 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Oct 30, 2017

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

Status: Open.

#14 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Oct 29, 2017

TLAPS fails to prove instances of temporal theorems

bug

Status: Open.

#11 In tlaplus/tlapm_alternative_parser_experiment;

· muenchnerkindl opened on Sep 4, 2017

Theorems from instantiated modules

Status: Open.

#9 In tlaplus/tlapm_alternative_parser_experiment;

· johnyf opened on Jul 19, 2017