Markus Alexander Kuppe
Markus Alexander Kuppe
https://lamport.azurewebsites.net/tla/current-tools.pdf has an independent lifecycle of the source code. Let's unify the source and its documentation, and make it more organic. [current-tools.tex.txt](https://github.com/tlaplus/tlaplus/files/7296101/current-tools.tex.txt)
In `tlc2.tool.impl.Tool.getActionsAppl(OpApplNode, Context, OpDefNode, CostModel)` ```tla ----- MODULE Github672 ----- VARIABLES v Init == v = TRUE Next == \E b \in BOOLEAN : \* Substituting BOOLEAN for {TRUE} below...
```java java.lang.ArrayIndexOutOfBoundsException: Index 4223 out of bounds for length 1 at tlc2.tool.ConcurrentTLCTrace$Record.getRecord(ConcurrentTLCTrace.java:306) at tlc2.tool.ConcurrentTLCTrace.getTrace(ConcurrentTLCTrace.java:92) at tlc2.tool.ModelChecker.getTraceInfo(ModelChecker.java:1064) at tlc2.module.TLCExt.getTrace(TLCExt.java:243) at tlc2.value.impl.EvaluatingValue.eval(EvaluatingValue.java:72) at tlc2.tool.impl.Tool.evalApplImpl(Tool.java:1865) at tlc2.tool.impl.CallStackTool.evalAppl(CallStackTool.java:170) at tlc2.tool.impl.Tool.evalImpl(Tool.java:1632) at tlc2.tool.impl.CallStackTool.eval(CallStackTool.java:142) at tlc2.value.impl.OpValue.eval(OpValue.java:22)...
Checking the following liveness property for EWD998 causes the error below. ```tla ENABLED \E i \in Node:
The PlusCal translator could generate a `PCOK` from the set of possible pc values that is manually added as a conjunct in a user-provided `TypeOK`, and that is robust against...
Commit b778fec5e086de2a2b9e458c1f375193f4d952e1 changes `tlc2.tool.impl.SpecProcessor.processActionConstraints()` to assert that no value has been set for the body of the action-constraint. ```java TLC2 Version 2.16 of Day Month 20?? Running breadth-first search Model-Checking...
Originally reported on the mailinglist: http://discuss.tlapl.us/msg04080.html ```shell $ tlc MC.tla -workers 64 -cleanup -nowarning -deadlock TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99) Running breadth-first search Model-Checking with fp...
@xxyzzn: "The PlusCal translator should report an error if one process uses a variable declared as a local variable of another process but not as a local variable of the...
LL: "TLC constructs the state graph, except the nodes are fingerprints of the states rather than the states. On an error, TLC constructs the error trace by re-executing the spec...
`lsp4j.debug` depends on xtext base at runtime, because the generated POJOs [import](https://github.com/eclipse/lsp4j/blob/9ae5b3c05eecdd75ec6d3154d17f871fcd124fa5/org.eclipse.lsp4j.generator/src/main/java/org/eclipse/lsp4j/generator/JsonRpcDataProcessor.xtend#L151-L161) `org.eclipse.xtext.xbase.lib.Pure` and `org.eclipse.xtext.xbase.lib.util.ToStringBuilder`. Neither `@Pure` nor `ToStringBuilder` are required by `lsp4j.debug`'s functionality. Please consider removing the xtext dependency...