Regression test 11 fails

[paschembri]

Hello, thank you for sharing PlusPy.

I just cloned the repository and tried to run tests with ./regres.scr and the test 11 failed. I tried to run directly ./pluspy -S0 -c100 Exprs and I got can't load TLC : fatal error.

I believe the TLC module is missing. I'll link a pull request.

[lemmy]

It has been renamed to TLCExt

[paschembri]

Mmm. I cannot make the test 11 succeed when renaming TLC to TLCExt. However, with the TLC.tla file it does work... TLCExt misses SortSeq used in Exprs.tla.

[lemmy]

PlusPy should indeed use TLC's version of TLC.tla. The operators JSignal, JSignalReturn, and JWait should be added to TLCExt.tla of the CommunityModules to make sure tools stay compatible.

[lemmy]

Places that have to be checked:

markus@avocado:PlusPy(master)$ grep -r TLC .
./pluspy.py:        return "TLC!Assert(_, _)"
./pluspy.py:        return "TLC!JavaTime()"
./pluspy.py:        return "TLC!Print(_)"
./pluspy.py:        return "TLC!TPrint(_)"
./pluspy.py:        return "TLC!RandomElement(_)"
./pluspy.py:        return "TLC!ToString(_)"
./pluspy.py:TLCvars = {}
./pluspy.py:class TLCSetWrapper(Wrapper):
./pluspy.py:        return "TLC!TLCSet(_, _)"
./pluspy.py:        TLCvars[args[0]] = args[1]
./pluspy.py:class TLCGetWrapper(Wrapper):
./pluspy.py:        return "TLC!TLCGet(_)"
./pluspy.py:        return TLCvars[args[0]]
./pluspy.py:wrappers["TLC"] = {
./pluspy.py:    "TLCSet": TLCSetWrapper(),
./pluspy.py:    "TLCGet": TLCGetWrapper(),
./pluspy.py:        return "TLC!JWait(_)"
./pluspy.py:        return "TLC!JSignalReturn(_,_)"
./pluspy.py:wrappers["TLC"] = {
./README.md:Using the new JWait/JSignalReturn interfaces in TLC, threads can use
./README.md:They can be used with the TLC model checker or TLAPS to validate your code.  The
./modules/lib/TLCExt.tla:------------------------------- MODULE TLCExt ----------------------------------
./modules/lib/TLCExt.tla:\* This module provides some compatibility with the TLC module
./modules/lib/Bags.tla:EXTENDS TLC
./modules/lib/Bags.tla:  (* but rather one that TLC can evaluate.                                *)
./modules/other/BlockingQueueSplit.tla:EXTENDS Naturals, Sequences, FiniteSets, TLCExt
./modules/other/Exprs.tla:EXTENDS Integers, Sequences, FiniteSets, Bags, TLC
./modules/other/NBosco.tla:EXTENDS Naturals, FiniteSets, TLC
./modules/other/Bosco.tla:EXTENDS Naturals, FiniteSets, TLC
./modules/other/BinBosco.tla:EXTENDS Naturals, FiniteSets, TLC

[rvanren]

I forgot to add TLC.tla to the modules/lib directory. It's now there. Apologies. Thanks for trying it out and reporting the issue

[lemmy]

The following operators are currently both defined in TLC.tla and TLCExt.tla.

ToString(v) == (CHOOSE x \in [a : v, b : STRING] : TRUE).b
Print(out, val) == IF IOPut("fd", "stdout", out) THEN val ELSE val
PrintT(out) == Print(out, TRUE)

Any == CHOOSE x : x \notin { "Any" }

[rvanren]

I can probably remove those. Let me check

[rvanren]

Removed those lines. Thanks!