Proofs of integer properties

[chris...@gmail.com]

Hi,

I am trying to learn TLA+ by implementing some simple proofs. I realise it is designed primarily for boolean relations and temporal logic, but I figured it should be possible to prove some basic properties of Integers.

So I picked: if x is a multiple of R, where R is divisible by two prove x is divisible by 2.

I hit a number of issues, and I can't find a successful path to proof.

Specifically:

- I needed to add basic facts I thought should be "obvious" like a ^ b => b

- I had a lot of trouble taking proof steps relating to manipulation of equations eg. I had to define an axiom for a * b = b * a, and failed to prove or use the proof of a more complex fact, a * b * c = c * a * b

- Proofs requiring algebraic substitution only seem to work when the term to substitute is the first term, ie. if (1) x = A * B, I can prove the substition A = Y * Z into (1) == x = Y * Z * B, but not B = X * Y into (1) == x = A * Y * Z

Am I barking up the wrong tree here and using the wrong tool for this kind of proof? Or am I missing something?

Full proof follows.

Regards,
Chris.

(*
* We want to prove if x is divisible by and number R, that is divisible by 2, then x is divisible by 2
*)

EXTENDS Integers, TLAPS, TLC

CONSTANT N, R

(* Pick an arbitrary N >= 1 *)
ASSUME NAssumption == N \in Nat /\ N >= 1

(* R is any natural number that is a multiple of 2 *)
ASSUME RAssumption == R \in Nat /\ \E a \in Nat : R = 2 * a

VARIABLES x

XNat == x \in Nat
XChooseRN == x = R * N

(* X is a multiple N of R *)
Init == XNat ^ XChooseRN

(* We want to prove x is divisible by 2 *)
Result == \E y \in Nat : x = 2 * y

(* Some basic facts that the TLA+ solvers don't seem to know *)
AXIOM AndB == \A a,b : a ^ b => b
AXIOM NCommutatMult == \A a,b \in Nat : a * b <=> b * a

(*AXIOM NMultSubst == \A a,b,c,r \in Nat : (a = b * c) ^ (r = b * c) => (a = r)
AXIOM NMultSubst3 == \A a,b,c,d,r \in Nat : (r = a * b * c) ^ (d = b * c) => (r = a * d)

THEOREM NMultSubst3a == \A a,b,c,d,r : (d = b * c) => ((r = a * b * c) <=> (r = a * d))
<1> SUFFICES ASSUME NEW a, NEW b, NEW c, NEW d, NEW r,
d = b * c
PROVE (r = a * b * c) <=> (r = a * d)
OBVIOUS
<1> QED
*)

AXIOM NCommutatMult312 == \A a,b,c \in Nat : a * b * c = c * a * b
(* PROOF OMITTED*)

(* Try direct substitution *)
THEOREM XIsEven1 == Init => Result
<1> USE NAssumption, RAssumption DEF Init
<1> SUFFICES ASSUME Init PROVE Result
OBVIOUS
<1>2. x = R * N
BY Init, AndB DEF XNat, XChooseRN
<1>3. PICK q \in Nat : R = 2 * q
BY RAssumption, AndB
<1>4. x = 2 * q * N
BY <1>2, <1>3
<1>5. PICK y \in Nat : y = q * N
OBVIOUS
<1>6. x = 2 * y
BY <1>4, <1>5
<1> QED

(* Try to prove that by comparison *)
THEOREM XIsEven2 == Init => Result
<1> USE NAssumption, RAssumption DEF Init
<1> SUFFICES ASSUME Init PROVE Result
OBVIOUS
<1>2. x = R * N
BY Init, AndB DEF XNat, XChooseRN
<1>3. PICK q \in Nat : R = 2 * q
BY RAssumption, AndB
<1>4. x = 2 * q * N
BY <1>2, <1>3
<1>5. PICK y \in Nat : y = q * N
OBVIOUS
<1>6. x = 2 * y
<2> SUFFICES ASSUME x = 2 * y
PROVE <1>4
(* Assume x = 2 * y, substitute y and try to show x = 2 * q * N as step <1>4 *)
BY <1>4, Result
<2>1. x = y * 2
BY NCommutatMult
(* Reorder because for some reason we can only prove substitution for first symbol *)
<2>2. x = q * N * 2
BY <2>1, <1>5
<2>3. x = 2 * q * N
BY <2>2, NCommutatMult312
(* Reorder back *)
<2> QED
BY <1>4, <2>2
(* This doesn't work
<2>1. x = 2 * q * N
BY <1>5
<2> QED
BY <1>4, <2>1
*)
<1> QED

=============================================================================
\* Modification History
\* Last modified Wed Nov 05 11:30:16 PST 2014 by Chris.Nott
\* Created Tue Nov 04 11:05:21 PST 2014 by Chris.Nott

[TLA Plus]

Hi Chris,

I don't know why you expect a raised to the power b to imply b.  Perhaps you meant a conjoined with b, which is typed  a /\ b .  This might fix some of your other problems. 

You write

 if (1) x = A * B, I can prove the substition A = Y * Z into (1) == x = Y * Z * B, but not B = X * Y into (1) == x = A * Y * Z

I presume you mean that you can prove

   x = A * B  /\  A = Y * Z   =>  x = Y * Z * B

but can't prove

   x = A * B  /\  B = X * Y  =>  x = A * Y * Z

I don't know why you expect that to be true, but TLAPS does prove

   x = A * B  /\  B = X * Y  =>  x = A * X * Y

under the assumption that x, A, B, X, and Y are integers.  Note that this formula is not valid without that assumption.  On the other hand, the formula

      x = A * B  /\  B = X * Y  =>  x = A * (X * Y)

is valid without that assumption.

Leslie Lamport

  

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

Hi Chris,

below is a simple proof in TLAPS of what I believe is your intended result. As Leslie remarked, your difficulties seem to be caused by a confusion between /\ and ^, both of which appear to denote conjunction in your module.

LEMMA ASSUME NEW R \in Nat, \E a \in Nat : R = 2 * a,

             NEW N \in Nat, NEW VARIABLE x, x = R * N

      PROVE  \E y \in Nat : x = 2 * y

OBVIOUS

Note that it doesn't matter for the validity of this lemma if x is declared as a VARIABLE or CONSTANT.

And no, TLA+ is not primarily designed for reasoning about propositional logic (temporal or otherwise). Have you had a look at the Hyperbook?

Regards,

Stephan

[fl]

> Le jeudi 6 novembre 2014 09:14:11 UTC+1, Stephan Merz a écrit :

> below is a simple proof in TLAPS of what I believe is your intended result.

 

By the way Stephan, your book about temporal logic [1] is not available at Gibert's  (it is not referenced).

It is available at Eyrolles'?  I ask this because, it will save me a walk.

 

[1] "Temporal logic and state systems".

 

--

FL

[chris...@gmail.com]

Hi, yes this is the cause of my problems.

I appreciate your response and Stephan's. My proof now works.

One thing I don't fully understand is after I reduced Init to x = R * N, the proof was still polluted somewhere by the use of ^ instead of /\ even though it should have been left unexpanded as Init == XNat ^ XChooseRN and not affected proof involving x. But anyway a relatively straightforward mistake. Now I can go on to make more interesting mistakes, thanks.

[chris...@gmail.com]

Hi again,

Yes I am reading through the hyperbook. I am working through Euclid's algorithm (PlusCal) right now, I am having some trouble:

1) GCD3 theorem information in the text seems to suggest the following should work:
==========================
THEOREM GCD3 == \A m, n \in Number : (n > m) => (GCD(m, n) = GCD(m, n-m))
  <1> SUFFICES ASSUME NEW m \in Number, NEW n \in Number,
                      n > m
               PROVE  GCD(m, n) = GCD(m, n-m)
    OBVIOUS
  <1>1.  \A i \in Int : Divides(i, m) /\ Divides(i, n)
                      <=> Divides(i, m) /\ Divides(i, n - m)
    BY LemmaDiv DEF Divides
  <1> QED
    BY DEF GCD, SetMax, DivisorsOf, Divides
==========================
But <1>1 doesn't prove. I probably misunderstood.

2) The proofs section breaking down Inv /\ [Next]_vars => Inv', I needed to add 'BY UNCHANGED vars' to steps <2>2 and <2>3. It didn't seem to pick it up from ASSUMES, and I didn't see anything in the text about it.

3) I couldn't get a TLC model to run with the Euclid PlusCal module. It just won't start, no error messages or anything. I had a model running for GCD module just fine.

4) I saw an assertion when I accidentally put a proof step <1>4 in USE DEF <1>4 instead of USE <1>4 DEF ..  I assumed it was not surprising this caused weirdness.

In general I am really impressed with the quality of the environment and the documentation. I have wanted to look into using formal methods for a while but the literature is almost incomprehensible. You really need to just dive in and play with it, but then the trick is finding tools etc. etc. For learning purposes it really helps to just be able to jump in, build a specification, test it against a model and then prove it.

One comment about the hyperbook in particular, the text description building up proofs is good to follow along and force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

Regards,
Chris.

[Stephan Merz]

Hi Chris,

1) GCD3 theorem information in the text seems to suggest the following should work:
==========================
THEOREM GCD3 == \A m, n \in Number : (n > m) => (GCD(m, n) = GCD(m, n-m)) 
  <1> SUFFICES ASSUME NEW m \in Number, NEW n \in Number,
                      n > m
               PROVE  GCD(m, n) = GCD(m, n-m)
    OBVIOUS
  <1>1.  \A i \in Int : Divides(i, m) /\ Divides(i, n) 
                      <=> Divides(i, m) /\ Divides(i, n - m)
    BY LemmaDiv DEF Divides
  <1> QED
    BY DEF GCD, SetMax, DivisorsOf, Divides
==========================
But <1>1 doesn't prove. I probably misunderstood.

I'm not quite sure which part of the hyperbook you looked at. The informal proof in the main track has four steps and uses lemma Div. The formal proof in the proof track (chapter 11.2) doesn't mention that lemma: in fact, the SMT backend is smart enough to perform that reasoning. Reconstructing the lemma from what is written in the hyperbook, I obtain

THEOREM GCD3 == \A m,n \in Nat \ {0} : (n > m) => (GCD(m, n) = GCD(m, n - m))

<1>. SUFFICES ASSUME NEW m \in Nat \ {0}, NEW n \in Nat \ {0}, n > m

              PROVE  GCD(m, n) = GCD(m, n - m)

  OBVIOUS

<1>. \A i \in Int : Divides(i,m) /\ Divides(i,n)

                <=> Divides(i,m) /\ Divides(i, n - m)

  BY DEF Divides

<1>. QED  BY DEF GCD, SetMax, DivisorsOf

and this is indeed proved. It's very similar to what you wrote except that (a) I don't invoke LemmaDiv, (b) all steps are unnumbered, and (c) I use Nat and Int whereas you have Number and Int. Let's look at each difference:

(a) Adding LemmaDiv (whatever it may be) might confuse the backend but it seems unlikely that this is the problem.

(b) It's obvious that you need to add <1>1 as a fact to the proof of the QED step, but that doesn't affect the proof of your step <1>1.

(c) This must be the real difference: you should expand the definition of Number, otherwise the prover cannot apply the definition of Divides, which (according to the hyperbook) is stated for Int.

Anyway, I attach my full module to this message so that we are on the same page.

2) The proofs section breaking down Inv /\ [Next]_vars => Inv', I needed to add 'BY UNCHANGED vars' to steps <2>2 and <2>3. It didn't seem to pick it up from ASSUMES, and I didn't see anything in the text about it.

I don't quite see where you are pointing since the hyperbook doesn't seem to show all the details of that proof but I presume that the assumption UNCHANGED vars appears the step enclosing the one you are trying to prove. You have to invoke that step in the facts that appear in the BY clause, as in:

<4>42. ASSUME Inv, UNCHANGED vars PROVE Inv'

  BY <4>42 DEF Inv, vars

The basic principle is that all necessary facts and definitions have to be named explicitly in proofs, except for those mentioned in a USE [DEF] clause or for facts in unnumbered steps that cannot be named. The apparently circular reference <4>42 in the step above refers to the assumption of the current step. References to <4>42 outside of its own proof refer to the entire ASSUME PROVE clause.

By the way, the module attached to this message contains a simpler proof of the theorem: the decompositions introduced in the hyperbook are given for pedagogical purposes.

3) I couldn't get a TLC model to run with the Euclid PlusCal module. It just won't start, no error messages or anything. I had a model running for GCD module just fine.

I cannot reproduce this problem. More specifically, I can run TLC on the module attached to this message. Concretely, I instantiated M and N by 42 and 24 and told TLC to verify the invariants Inv and PartialCorrectness. As expected, TLC complains that it cannot enumerate Int, so I have to override the definition of Int (in Advanced Options -> Definition Override), for example by the interval -100 .. 100.

4) I saw an assertion when I accidentally put a proof step <1>4 in USE DEF <1>4 instead of USE <1>4 DEF ..  I assumed it was not surprising this caused weirdness. 

Yes, this should eventually be caught by the proof manager instead of raising an assertion ...

In general I am really impressed with the quality of the environment and the documentation. I have wanted to look into using formal methods for a while but the literature is almost incomprehensible. You really need to just dive in and play with it, but then the trick is finding tools etc. etc. For learning purposes it really helps to just be able to jump in, build a specification, test it against a model and then prove it.

Thanks. Feedback is important to improve the tool and the doc.

One comment about the hyperbook in particular, the text description building up proofs is good to follow along and force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

It might be helpful to have the actual TLA+ modules accompany the hyperbook, rather than just the PDF versions (even the ASCII in PDF form).

Regards,

Stephan

[chris...@gmail.com]

On Saturday, November 8, 2014 8:44:23 AM UTC-8, Stephan Merz wrote:

Hi Chris,

1) GCD3 theorem information in the text seems to suggest the following should work:
==========================

 <snip>

 

I'm not quite sure which part of the hyperbook you looked at. The informal proof in the main track has four steps and uses lemma Div. The formal proof in the proof track (chapter 11.2) doesn't mention that lemma: in fact, the SMT backend is smart enough to perform that reasoning. Reconstructing the lemma from what is written in the hyperbook, I obtain

I was looking at both. I may have confused myself.
 

THEOREM GCD3 == \A m,n \in Nat \ {0} : (n > m) => (GCD(m, n) = GCD(m, n - m))

<1>. SUFFICES ASSUME NEW m \in Nat \ {0}, NEW n \in Nat \ {0}, n > m

              PROVE  GCD(m, n) = GCD(m, n - m)

  OBVIOUS

<1>. \A i \in Int : Divides(i,m) /\ Divides(i,n)

                <=> Divides(i,m) /\ Divides(i, n - m)

  BY DEF Divides

<1>. QED  BY DEF GCD, SetMax, DivisorsOf

and this is indeed proved. It's very similar to what you wrote except that (a) I don't invoke LemmaDiv, (b) all steps are unnumbered, and (c) I use Nat and Int whereas you have Number and Int. Let's look at each difference:

(a) Adding LemmaDiv (whatever it may be) might confuse the backend but it seems unlikely that this is the problem.

(b) It's obvious that you need to add <1>1 as a fact to the proof of the QED step, but that doesn't affect the proof of your step <1>1.

(c) This must be the real difference: you should expand the definition of Number, otherwise the prover cannot apply the definition of Divides, which (according to the hyperbook) is stated for Int.

Thank you! I was wondering why I couldn't get Number to work, and of course I am not expanding its definition. I had already rewritten it to use Nat \ {0} but of course missed the QED BY <1>1.

Anyway, I attach my full module to this message so that we are on the same page.

2) The proofs section breaking down Inv /\ [Next]_vars => Inv', I needed to add 'BY UNCHANGED vars' to steps <2>2 and <2>3. It didn't seem to pick it up from ASSUMES, and I didn't see anything in the text about it.

I don't quite see where you are pointing since the hyperbook doesn't seem to show all the details of that proof but I presume that the assumption UNCHANGED vars appears the step enclosing the one you are trying to prove. You have to invoke that step in the facts that appear in the BY clause, as in:

<4>42. ASSUME Inv, UNCHANGED vars PROVE Inv'

  BY <4>42 DEF Inv, vars

The basic principle is that all necessary facts and definitions have to be named explicitly in proofs, except for those mentioned in a USE [DEF] clause or for facts in unnumbered steps that cannot be named. The apparently circular reference <4>42 in the step above refers to the assumption of the current step. References to <4>42 outside of its own proof refer to the entire ASSUME PROVE clause.

Yes thank you, this is the problem. I didn't realise you need to refer to the step's assumptions in the BY line. Most of my issues so far seem to be syntax errors and misunderstanding the scoping of rule inclusion.

By the way, the module attached to this message contains a simpler proof of the theorem: the decompositions introduced in the hyperbook are given for pedagogical purposes.

3) I couldn't get a TLC model to run with the Euclid PlusCal module. It just won't start, no error messages or anything. I had a model running for GCD module just fine.

I cannot reproduce this problem. More specifically, I can run TLC on the module attached to this message. Concretely, I instantiated M and N by 42 and 24 and told TLC to verify the invariants Inv and PartialCorrectness. As expected, TLC complains that it cannot enumerate Int, so I have to override the definition of Int (in Advanced Options -> Definition Override), for example by the interval -100 .. 100.

I give up. Your modules model check just fine. My euclid module, which is almost identical to yours, simply refuses to. I guess there must be something screwy in my environment. I tried literally copying the contents of your files into mine, running a model check and it still won't run.

4) I saw an assertion when I accidentally put a proof step <1>4 in USE DEF <1>4 instead of USE <1>4 DEF ..  I assumed it was not surprising this caused weirdness. 

Yes, this should eventually be caught by the proof manager instead of raising an assertion ...

In general I am really impressed with the quality of the environment and the documentation. I have wanted to look into using formal methods for a while but the literature is almost incomprehensible. You really need to just dive in and play with it, but then the trick is finding tools etc. etc. For learning purposes it really helps to just be able to jump in, build a specification, test it against a model and then prove it.

Thanks. Feedback is important to improve the tool and the doc.

One comment about the hyperbook in particular, the text description building up proofs is good to follow along and force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

It might be helpful to have the actual TLA+ modules accompany the hyperbook, rather than just the PDF versions (even the ASCII in PDF form).

Agreed.
 

Regards,

Stephan

[Leslie Lamport]

   One comment about the hyperbook in particular, the text description building up proofs is good to follow along and
   force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

 

   It might be helpful to have the actual TLA+ modules accompany the hyperbook, rather than just the PDF versions (even the ASCII in PDF form).

   Agreed.

In general, I have tried to present a complete module after developing it bit by bit.  However, sometimes a module isn't developed bit by bit, but a first version is developed, then it is modified to form another version, then modified again and again.  So, instead of having a single complete module, there are quite a few.  In those cases, it seems impractical to provide a complete module for each of those versions.  Perhaps someone has a suggestion on what to do in that case.  However, it is possible that there are places where it would be reasonable to provide a complete module (or perhaps a complete proof) and I have failed to do so.  I would appreciate having those exact places pointed out.

Thanks,

Leslie

[tlapl...@lemmster.de]

On 10.11.2014 20:13, chris...@gmail.com wrote:
> I cannot reproduce this problem. More specifically, I can run TLC on
> the module attached to this message. Concretely, I instantiated M
> and N by 42 and 24 and told TLC to verify the invariants Inv and
> PartialCorrectness. As expected, TLC complains that it cannot
> enumerate Int, so I have to override the definition of Int (in
> Advanced Options -> Definition Override), for example by the
> interval -100 .. 100.
>
>
> I give up. Your modules model check just fine. My euclid module, which
> is almost identical to yours, simply refuses to. I guess there must be
> something screwy in my environment. I tried literally copying the
> contents of your files into mine, running a model check and it still
> won't run.

Hi Chris,

can you share the disk content¹ of your spec/model including the nested
*.toolbox directory? Then I can (locally) debug why TLC won't run on it.

Cheers
Markus

¹ The path is shown at the top of the spec editor.

[chris...@gmail.com]

The specific proof I got stuck on was the full proof (proof track) of Euclid's algorithm, where you decompose Inv /\ [Next]_vars.

First I got stuck for a while getting it to decompose the same way as you described, then after I got the decomposed proof stages to match I hit the above problems trying to prove.

This proof is quite useful because it is the first proof I saw that walks through the full process generating a specification using PlusCal to full proof. For that reason I think it is worth including the final text of this proof.

It wouldn't hurt to have a repository of examples linked directly off the website, rather than including all examples with the book. I keep losing track where I found various interesting proofs, in TLAPS examples, papers or one of the books. For certain proofs like Euclid's algorithm it is valuable to have several proofs that take different approaches to contrast.

[chris...@gmail.com]

Attached.

[Markus Alexander Kuppe]

On 12.11.2014 00:28, chris...@gmail.com wrote:
>
> Hi Chris,
>
> can you share the disk content¹ of your spec/model including the nested
> *.toolbox directory? Then I can (locally) debug why TLC won't run on
> it.
>
> Cheers
> Markus
>
> ¹ The path is shown at the top of the spec editor.
>
>
> Attached.

Hi Chris,

all four Euclid models can be successfully checked with TLC here. The
only parts I had to adapt are the mappings to TLAPS' standard modules
(I'm on Linux).
Is there anything helpful in the .log file located in the Toolbox's
installation directory under workspace/.metadata/?

Markus

[chris...@gmail.com]

Hi Markus, it looks to me like maybe there is some sort of naming case problem. It complains about GCD resource exists with different case gcd. I may have started development with it called GCD and renamed it so it may have cached this version of the name somewhere. I can't see anywhere in the current version of the files that calls the module GCD, though the gcd module does contain a GCD definition.

I tried deleting the gcd and euclid_pluscal  toolbox and tlaps dirs and it worked after I deleted the euclid_pluscal dirs.

Regards,
Chris.


Logs below.

!ENTRY org.lamport.tla.toolbox 4 0 2014-11-13 10:38:17.053

!MESSAGE Error creating resource link to C:\work\docs\tla\gcd.tla

!STACK 1

org.eclipse.core.internal.resources.ResourceException: A resource exists with a different case: '/euclid_pluscal/GCD.tla'.

    at org.eclipse.core.internal.resources.Resource.checkDoesNotExist(Resource.java:308)

    at org.eclipse.core.internal.resources.Resource.assertLinkRequirements(Resource.java:155)

    at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:649)

    at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:623)

    at org.lamport.tla.toolbox.util.ResourceHelper.getLinkedFile(ResourceHelper.java:383)

    at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:317)

    at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:84)

    at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:57)

    at org.lamport.tla.toolbox.spec.parser.SpecificationParserLauncher.parseSpecification(SpecificationParserLauncher.java:38)

    at org.lamport.tla.toolbox.spec.nature.ParserHelper$2.run(ParserHelper.java:75)

    at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2344)

    at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2326)

    at org.lamport.tla.toolbox.spec.nature.ParserHelper.rebuildSpec(ParserHelper.java:84)

    at org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.build(TLAParsingBuilder.java:81)

    at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:728)

    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)

    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:199)

    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:239)

    at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:292)

    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)

    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:295)

    at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:351)

    at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:374)

    at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:143)

    at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:241)

    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)

!SUBENTRY 1 org.eclipse.core.resources 4 275 2014-11-13 10:38:17.054

!MESSAGE A resource exists with a different case: '/euclid_pluscal/GCD.tla'.



!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:17.071

!MESSAGE Resulting status is:  parsed
... build invocation finished.



!ENTRY org.lamport.tla.toolbox.tool.tlc.ui 4 0 2014-11-13 10:38:17.807

!MESSAGE Error launching the configuration euclid_pluscal___Model_3

!STACK 1

org.eclipse.core.internal.resources.ResourceException: Resource '/euclid_pluscal/gcd.tla' does not exist.

    at org.eclipse.core.internal.resources.Resource.checkExists(Resource.java:320)

    at org.eclipse.core.internal.resources.Resource.checkAccessible(Resource.java:194)

    at org.eclipse.core.internal.resources.Resource.checkAccessibleAndLocal(Resource.java:200)

    at org.eclipse.core.internal.resources.Resource.checkCopyRequirements(Resource.java:232)

    at org.eclipse.core.internal.resources.Resource.assertCopyRequirements(Resource.java:139)

    at org.eclipse.core.internal.resources.Resource.copy(Resource.java:540)

    at org.lamport.tla.toolbox.tool.tlc.launch.TLCModelLaunchDelegate.buildForLaunch(TLCModelLaunchDelegate.java:294)

    at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:822)

    at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:703)

    at org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor.launchModel(ModelEditor.java:688)

    at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage.doRun(BasicFormPage.java:783)

    at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage$RunAction.run(BasicFormPage.java:858)

    at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)

    at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)

    at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)

    at org.eclipse.jface.action.ActionContributionItem$6.handleEvent(ActionContributionItem.java:452)

    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)

    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1053)

    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4165)

    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3754)

    at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2696)

    at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2660)

    at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2494)

    at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:674)

    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)

    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:667)

    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)

    at org.lamport.tla.toolbox.Application.start(Application.java:41)

    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)

    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)

    at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)

    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:344)

    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)

    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)

    at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)

    at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)

    at java.lang.reflect.Method.invoke(Unknown Source)

    at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)

    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)

    at org.eclipse.equinox.launcher.Main.run(Main.java:1410)

!SUBENTRY 1 org.eclipse.core.resources 4 368 2014-11-13 10:38:18.250

!MESSAGE Resource '/euclid_pluscal/gcd.tla' does not exist.



!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:18.295

!MESSAGE Spec build invoked on euclid_pluscal ...



!ENTRY org.lamport.tla.toolbox 4 0 2014-11-13 10:38:19.437

!MESSAGE Error creating resource link to C:\work\docs\tla\gcd.tla

!STACK 1

org.eclipse.core.internal.resources.ResourceException: A resource exists with a different case: '/euclid_pluscal/GCD.tla'.

    at org.eclipse.core.internal.resources.Resource.checkDoesNotExist(Resource.java:308)

    at org.eclipse.core.internal.resources.Resource.assertLinkRequirements(Resource.java:155)

    at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:649)

    at org.eclipse.core.internal.resources.Resource.createLink(Resource.java:623)

    at org.lamport.tla.toolbox.util.ResourceHelper.getLinkedFile(ResourceHelper.java:383)

    at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:317)

    at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:84)

    at org.lamport.tla.toolbox.spec.parser.ModuleParserLauncher.parseModule(ModuleParserLauncher.java:57)

    at org.lamport.tla.toolbox.spec.parser.SpecificationParserLauncher.parseSpecification(SpecificationParserLauncher.java:38)

    at org.lamport.tla.toolbox.spec.nature.ParserHelper$2.run(ParserHelper.java:75)

    at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2344)

    at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2326)

    at org.lamport.tla.toolbox.spec.nature.ParserHelper.rebuildSpec(ParserHelper.java:84)

    at org.lamport.tla.toolbox.spec.nature.TLAParsingBuilder.build(TLAParsingBuilder.java:81)

    at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:728)

    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)

    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:199)

    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:239)

    at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:292)

    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)

    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:295)

    at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:351)

    at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:374)

    at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:143)

    at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:241)

    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)

!SUBENTRY 1 org.eclipse.core.resources 4 275 2014-11-13 10:38:19.443

!MESSAGE A resource exists with a different case: '/euclid_pluscal/GCD.tla'.



!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:19.494

!MESSAGE Resulting status is:  parsed
... build invocation finished.



!ENTRY org.lamport.tla.toolbox 1 -1 2014-11-13 10:38:26.029

!MESSAGE Removed a parse result listener.There are now 0 listeners.