How to build Codeplex Tlaplus Tools?

[marc magrans de abril]

Dear Tlaplus Tools experts,

I have performed the following steps:

* Cloned the Git repo in https://tlaplus.codeplex.com/

* Compile the default target of the customBuild.xml file under tlaplus/tlatools

* This generates a tla2tools.jar

I wonder if that's all I need to compile all the tools. Is it?

Do you have any instructions on the procedure to compile and run a new version?

Have I compiled all the tools (i.e. TLC, SANY, etc.)?

What should I do to run this new version in my OSX?

Thanks,

Marc

[Markus Alexander Kuppe]

Hi Marc,

if you just want the tools [1] but don't want the TLA Toolbox [2],
tla2tools.jar is all you really need (you could have downloaded [1] the
tools from the web instead of compiling manually).

In order to run the individual tools, just add tla2tools.jar to java's
classpath:

java -cp tla2tools.jar tlc2.TLC
java -cp tla2tools.jar tla2sany.SANY
java -cp tla2tools.jar pcal.trans
java -cp tla2tools.jar tla2tex.TLA

When it comes to the tools' arguments, the source files directly are a
good source of information. See tlc2.TLC [3], pcal.trans [4],
tla2sany.SANY [5] and tla2tex.TLA [6].


May I ask why you don't want to use the Toolbox [2]? It provides an easy
entry into TLA+ and a graphical front-end for the tools.

Cheers
Markus

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html
[3]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tlc2/TLC.java
[4]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/pcal/trans.java
[5]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tla2sany/drivers/SANY.java
[6]
http://tlaplus.codeplex.com/SourceControl/latest#tlatools/src/tla2tex/TLA.java

[marc magrans de abril]

Hi,

>>java -cp tla2tools.jar tlc2.TLC 

>>java -cp tla2tools.jar tla2sany.SANY 
>>java -cp tla2tools.jar pcal.trans 
>>java -cp tla2tools.jar tla2tex.TLA 

Interesting, I didn't know that.

>>May I ask why you don't want to use the Toolbox [2]? It provides an easy  entry into TLA+ and a graphical front-end for the tools. 

I guess that I didn't explain myself well enough. 

In fact, I'm pretty happy with the Toolbox look and feel.

What I would like is to use the recompiled version of tla2tools.jar on the Toolbox. How should I tell to the Toolbox to use the recompiled version of tla2tools.jar (i.e. copy the file to some directory, change some preferences, etc.)? 

Thanks,

Marc

[Markus Alexander Kuppe]

On 08.03.2015 22:36, marc magrans de abril wrote:
> What I would like is to use the recompiled version of tla2tools.jar on
> the Toolbox. How should I tell to the Toolbox to use the recompiled
> version of tla2tools.jar (i.e. copy the file to some directory, change
> some preferences, etc.)?

Hi Marc,

if you have made changes to the source and want to run a customized
tla2tools.jar with the Toolbox, it's easiest to rebuild the Toolbox from
scratch. Its build will recompile its embedded¹ tla2tools.jar automatically.

In order to build the Toolbox and its embedded tla2tools, run "mvn
verify" from the root of the git repository. You will need Apache maven
3.0.x and a recent JDK. To skip the Toolbox's UI tests, it's "mvn verify
-Dmaven.test.skip=true".
You will find the Toolbox zips in
org.lamport.tla.toolbox.product.product/target/products/ relative to the
root of the git repository.


Can you say what kind of code changes you have made?

Cheers
Markus

¹ The embedded tla2tools.jar is technically shaped differently than the
standalone tla2tools.jar.

[marc magrans de abril]

Hi,

>>Can you say what kind of code changes you have made?

I'm not sure if I will have the time or the skill to make it happen. However, If I had both, I would like to fix the simulation issue with Liveness. Simulation is pretty useful when the state space is too big, even if incomplete.

If I had even more time, I would like to have Floats (!= Reals). I'm aware that floats imply an awful explosion in sate space. However, I think that it could still be useful to use simulation in this case. As I said, just a wish, and I can even imagine that it is not even possible.

In summary just ideas and a small amount of time.

In any case, thanks for the instructions!

Cheers,
Marc

[Markus Alexander Kuppe]

On 09.03.2015 09:32, marc magrans de abril wrote:
> I'm not sure if I will have the time or the skill to make it happen.
> However, If I had both, I would like to fix the simulation issue with
> Liveness. Simulation is pretty useful when the state space is too big,
> even if incomplete.
>

> [...]

>
> In summary just ideas and a small amount of time.

Hi Marc,

in order to use your time most efficiently, consider following the
"mku-liveness" branch. It's where I'm working on TLC's liveness
implementation myself. I'd assume it is best if we even occasionally
touch base.

Cheers
Markus

[Markus Alexander Kuppe]

On 09.03.2015 09:32, marc magrans de abril wrote:
>
> I'm not sure if I will have the time or the skill to make it happen.
> However, If I had both, I would like to fix the simulation issue with
> Liveness. Simulation is pretty useful when the state space is too big,
> even if incomplete.
>
> If I had even more time, I would like to have Floats (!= Reals). I'm
> aware that floats imply an awful explosion in sate space. However, I
> think that it could still be useful to use simulation in this case. As I
> said, just a wish, and I can even imagine that it is not even possible.
>
> In summary just ideas and a small amount of time.
>
> In any case, thanks for the instructions!

Hi Marc,

can you elaborate on the issues you have with Liveness in simulation
mode? As I said, I'm working on Liveness right now and might have a
chance to address your problems with simulation mode too.

Thanks
Markus

[Marc Magrans de Abril]

Hi,

Some time ago I realized about the problem: https://groups.google.com/forum/#!searchin/tlaplus/liveness$20simulation/tlaplus/MBjAaNbNMMc/qvp4wtoi9pEJ

I have not further investigated the issue. 

Cheers,

---

Marc Magrans de Abril

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/XLAfgMVAu38/unsubscribe.
To unsubscribe from this group and all its topics, 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.

[Leslie Lamport]

Hi Marc and everyone else reading this,

When I discovered the problem, it seemed to me that liveness checking
simply didn't work in simulation mode and I didn't bother recording
the examples on which I tried it.  Now, we've been unable to reproduce
the problem.  We'd appreciate it if people could try using simulation
mode to check a model specifying a liveness property and let us know
what happens.

Leslie

[marc magrans de abril]

Hi,

Today, I just tried a simple example (see below) were an integer is incremented by 1 (modulo 100). The model checker finds the error on Liveness1 and Liveness2 properties. However, the simulator does not find them.

Is this a bug, or just something not understood on my side?

Cheers,

Marc

------------------------------ MODULE Example1 ------------------------------

EXTENDS Integers

VARIABLE x

Init == x = 0

Next == x' = ( x + 1 ) % 100

Spec == Init /\ [][Next]_<<x>> /\ []<><<TRUE>>_<<x>> 

Liveness1 == <>(x = -1000)

Liveness2 == <>(x = 101)

=============================================================================

[Markus Alexander Kuppe]

On 30.03.2015 08:58, marc magrans de abril wrote:
> Today, I just tried a simple example (see below) were an integer is
> incremented by 1 (modulo 100). The model checker finds the error on
> Liveness1 and Liveness2 properties. However, the simulator does not find
> them.
>
> Is this a bug, or just something not understood on my side?

Hi Marc,

the problem is not a bug in simulation mode. Simulation - by default -
checks behaviors up to a length of 100 states. This is too short for
your invariants. Try increasing the "Maximum length of a trace" to more
than 100 states on the "Advanced Options" page of the Model editor.

Regular model checking obviously does not restrict behaviors to a
maximum length.

Cheers
Markus

[Marc Magrans de Abril]

Silly me :) 

Thanks!