TLAPM Error

Hello, When I used TLA+ proof system, I met the following error: Oops, this seems to be a bug in TLAPM. Please give feedback to developers. Failure("Module.Parser.parse_file") Raised at file ...

Id #44 | Release: None | Updated: Apr 26 at 10:04 AM by MartinRie | Created: Apr 24 at 1:52 AM by lxh1002

Unable to install TLAPS on Ubuntu 16.04

I changed the file's permissions, and attempted to run it, but I keep getting the following error: $ ./tlaps-install.bin bash: ./tlaps-install.bin: No such file or directory Is it something to d...

Id #43 | Release: None | Updated: Oct 6, 2016 at 7:47 PM by omazhary | Created: Oct 5, 2016 at 6:54 PM by omazhary

Erroneous encoding of hypotheses involving primed variables

Sequents that have VARIABLE parameters, which occur primed in the hypotheses are translated inconsistently for the backends, making it impossible to apply them to prove anything. A minimal example ...

Id #42 | Release: None | Updated: Apr 20, 2016 at 11:45 AM by merz | Created: Apr 20, 2016 at 11:45 AM by merz

PM has problems with EXTENDS of submodules

Please consider a module with the following submodules: ------- MODULE inner ------ D(x) == x' USE DEF D ------- MODULE outer ------- EXTENDS inner LEMMA \A y : (D(y) = y') OBVIOUS * LEMMA \A y ...

Id #41 | Release: None | Updated: Jan 26, 2016 at 4:18 PM by MartinRie | Created: Jan 26, 2016 at 4:18 PM by MartinRie

No backend handles STRING

No backend is currently able to prove LEMMA "a" \in STRING OBVIOUS The Isabelle backend has a definition of STRING, but the constant is currently called String, and no automation is set up for...

Id #40 | Release: None | Updated: Jul 30, 2015 at 9:58 AM by merz | Created: Jul 30, 2015 at 9:58 AM by merz

Parametrized Module Instantiation with function argument is wrongly expanded (15-07-17)

Please consider the following auxiliary module: ------------------------- MODULE miniAbstractPaxos ------------------------- * uncomment all extends, to let the theorem Abstraction in minimal go th...

Id #39 | Release: None | Updated: Apr 20, 2015 at 5:13 PM by MartinRie | Created: Apr 20, 2015 at 4:50 PM by MartinRie

During module instantiation, a module variable is bound to the wrong term (2015-03-07)

At line 272 in the file NewBoundedBuffer occurs the proof step: <2> (a (+) 1) (-) b = (a (+) 1) (+) OMinus(b) BY OMinusDef, Z3 DEF ZN which expands to the obligation: ASSUME NEW CONSTANT Msg, ...

Id #38 | Release: None | Updated: Mar 10, 2015 at 3:03 PM by MartinRie | Created: Mar 10, 2015 at 3:03 PM by MartinRie

Quantifier instantiation not provable after unfolding definition (2015-03-09)

This is a bug reported by Leslie: The following Lemma with unfolded definition is not provable in SMT: P(x) == \A i_1, d_1 \in Int, r \in 0..x - 1 : i_1 = x * d_1 + r => d_1 = i_1 \div x /...

Id #37 | Release: None | Updated: Mar 10, 2015 at 2:49 PM by MartinRie | Created: Mar 10, 2015 at 9:54 AM by MartinRie

Infix operators in definitions (2015-03-05)

Checking the attached file with tlapm results in the error message: File "./MiniProducedConsumer.tla", line 32, characters 51-58: Error: arity mismatch tlapm ending abnormally with Failure("arity...

Id #36 | Release: None | Updated: Mar 10, 2015 at 2:50 PM by MartinRie | Created: Mar 9, 2015 at 3:44 PM by MartinRie

Obligation unfolding a definition from a module instance captures variables

This is a variation of Leslie's instantiation example from ch. 17.8 of the TLA book. When attempting to prove the lemma, tlapm generates the obligation ASSUME NEW VARIABLE z PROVE (ENABLED (z' # ...

Id #35 | Release: None | Updated: Mar 9, 2015 at 10:25 AM by MartinRie | Created: Feb 25, 2015 at 10:15 AM by MartinRie