[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] How to build Codeplex Tlaplus Tools?


>>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!


On Monday, March 9, 2015 at 8:47:07 AM UTC+1, Markus Alexander Kuppe wrote:
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
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?


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