| Remove branch parameter that breaks the badge. |
|
More...
|
about 2 months ago
|
| Small adjustments to the syntax to enhance consistency with the current styles. |
|
More...
|
about 2 months ago
|
| Move the implementation of `TLCStateStackFrame#matchesExpression` into `TLCSourceBreakpoint#matchesExpression` to privatize the member variable. |
|
More...
|
about 2 months ago
|
| Prevent instantiation of utility classes. |
|
More...
|
about 2 months ago
|
| Add TODO marker to indicate that error handling is incomplete. |
|
More...
|
about 2 months ago
|
| Remove all references to global static semantic error log |
|
More...
|
about 2 months ago
|
| Added license/copyright header to source files Misc other changes in response to PR feedback |
|
More...
|
about 2 months ago
|
| Initial support for ad-hoc/on-the-fly/dynamic Watch expressions. |
|
More...
|
about 2 months ago
|
| SANY: Moved methods around, removed unused fields |
|
More...
|
about 2 months ago
|
| Add `SpecProcessor#processConstantsDynamicExtendee`. |
|
More...
|
about 2 months ago
|
| Pass `Defns` a parameter to `SpecProcessors#processConstants` instead of accessing `SpecProcessors#defns`. |
|
More...
|
about 2 months ago
|
| For any string `str`, `TLCGet("-D" \o str)` equal the value that the Java system property `str` equals. Equals `"-D" \o str` if no system property by the name of `str` is defined. |
|
More...
|
about 2 months ago
|
| Debugger: Wrote unit test for breakpoint expressions. |
|
More...
|
about 2 months ago
|
| SANY: Expose parameter forcing exact match in SemanticNode#pathTo method. |
|
More...
|
2 months ago
|
| Prevent NPE in `SemanticNode#pathTo` when `SemanticNode` has no children. |
|
More...
|
2 months ago
|
| Make CommunityModules a test-time dependency of TLC. |
|
More...
|
2 months ago
|
| Given a breakpoint location, trace parse tree upward while recording all encountered identifiers that could be used in the breakpoint expression. |
|
More...
|
2 months ago
|
| Make deserializing previously unseen strings work |
|
More...
|
2 months ago
|
| SANY: Remove most static error logging usage Reduce usage of static SemanticNode#errors field Some additional places of use remain but this is a good incremental effort. Reduced usage count from 32 to 7. |
|
More...
|
2 months ago
|
| SANY: test context merge conflict error logging |
|
More...
|
2 months ago
|
| Add LevelNode#levelCheck API for public consumption Exposes Errors logging parameter for level-checking process Prior to these changes both semantic & level-checking used the same logging path, the static field SemanticNode.errors. Now the level-checking process will use the Errors parameter given as a method parameter instead. This reduces although does not yet eliminate usage of the global static SemanticNode.errors field. |
|
More...
|
2 months ago
|
| Basic support for breakpoint expressions in the TLC debugger. |
|
More...
|
2 months ago
|
| ArrayIndexOutOfBoundsException in TLA+ debugger during simulation if simulator eliminated finite stuttering from current trace. |
|
More...
|
2 months ago
|
| Fix typo: change 't0' to 'to' in README |
|
More...
|
3 months ago
|
| Re-defined constants are not "in-lined" but re-evaluated on *every* invocation (needs more aggressive constant propagation) |
|
More...
|
3 months ago
|
| Rename property as 'tlc2.tool.impl.ModelConfig.nosymmetry' |
|
More...
|
3 months ago
|
| Add java property 'nosymmetry' |
|
More...
|
3 months ago
|
| NPE when `-dumptrace` is not combined with `-debugger` because `Action` not stored in `TLCStateMut`. |
|
More...
|
3 months ago
|
| Include the position of the (TLC) Action parameters in `TLCGet("spec")` and `CounterExample` (if any). |
|
More...
|
3 months ago
|
| Add `-dumpTrace tlcaction` (with an optional filename) to dump the sequence of actions and their arguments/parameters leading to the counterexample. |
|
More...
|
3 months ago
|
