Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Trace expression evaluation with command-line TLC #393

Open
lemmy opened this issue Nov 14, 2019 · 73 comments
Open

Trace expression evaluation with command-line TLC #393

lemmy opened this issue Nov 14, 2019 · 73 comments

Comments

@lemmy
Copy link
Member

@lemmy lemmy commented Nov 14, 2019

Specific to-dos: A, B, C

Goal

Refactor TLC and Toolbox to make it possible to evaluate trace expressions with command-line TLC. In addition, the functionality should be reusable by third-party tools such as https://github.com/alygin/vscode-tlaplus.

User Experience/Proposal

From the implementation perspective it is easiest to generate SpecTE.tla and SpecTE.cfg (see below for details) when printing the original error trace (at this stage, all relevant information is available in the TLC Java model). A user would write TE.tla (TE extends SpecTE extends Spec) that defines actual trace expressions (e.g. the trace expression foo = tail - head where tail and head are vars of Spec.tla):

------------- MODULE TE -----------
EXTENDS SpecTE

VARIABLE foo

Init2323 == /\ init_15737066180447000
            /\ foo = tail - head
            
Next2323 == /\ next_15737066180448000
            /\ foo' = tail - head
            
=========================

A separate, dedicated module (TE.tla) has the advantage over command-line parameters that it can be checked into SCM and parsing errors can be reported; should we wish to support trace expressions supplied via a command line parameter, this TE.tla file could be generated in memory before SANY parses it.

An IDE such as vscode-tlaplus could generate a template for TE.tla, though it seems like two birds could be killed with one stone by having TLC accept a file that is a list of 1-N trace expressions and from this generate the TE.tla file in addition to the evaluation output. In this manner the user can have the file for SCM and future use, and third party applications / IDEs can be written to collect the trace expressions and provide those to TLC.

Current Toolbox implementation:

Reading regular error trace from MC.out into Toolbox's error view:

  1. Toolbox converts the trace in MC.out into org.lamport.tla.toolbox.tool.tlc.output.data.TLCState with an Eclipse based parser. TLCState and its imports do not depend on Eclipse code. Parsing should be straight forward to re-implemented without Eclipse code.

  2. Each TLCState gets added to org.lamport.tla.toolbox.tool.tlc.output.data.TLCError. TLCError is little more than a list except that it contains support to do paging of states (used when a trace is exceptionally long). TLCError and its imports have trivial dependencies on Eclipse code which don't prevent implementation in a non-Eclipse environment.

  3. Toolbox's error view gets states via org.lamport.tla.toolbox.tool.tlc.output.data.TLCError.getStates(Length) that more or less returns the underlying raw LinkedList.

Toolbox's error view to TE.tla/TE.cfg:

  1. When "Explore" is clicked in the Error-Trace Exploration section, org.lamport.tla.toolbox.tool.tlc.launch.TraceExplorerDelegate.buildForLaunch(ILaunchConfiguration, String, IProgressMonitor) does the following in the .toolbox directory:

    1. Removes previous TE-related files
    2. Creates new TE-related files (TE.tla, TA.cfg, ...)
    3. Copies Spec.tla
    4. Copies extended (either spec or Toolbox's error view) modules
    5. Converts the trace in MC_TE.out (which is a copy of MC.out) into a Vector of SimpleTLCState via org.lamport.tla.toolbox.tool.tlc.model.Model.getErrorTrace() TraceExplorerDelegate - this parsing relies on Eclipse code and, so, will need be re-implemented.
  2. The Vector from 1.5 above, the trace expressions, and the model definitions/constants/... are written to TE.tla and TE.cfg using org.lamport.tla.toolbox.tool.tlc.model.TraceExpressionModelWriter; this class does not depend on Eclipse code. The behavior spec, invariants, properties, constraints from the original model are ignored; it should be noted that org.lamport.tla.toolbox.tool.tlc.model.Model does depends on Eclipse code and would not be easily rewritten.

\* TRACE EXPLORER variable declaration @traceExploreExpressions
VARIABLES __trace_var_157369392033116000

...

\* TRACE NEXT definitiontraceExploreNext
next_157369392168618000 ==
/\ tail = 0
/\ pc = (worker1 :> "deq" @@ worker2 :> "deq" @@ worker3 :> "deq")
/\ disk = <<1>>
/\ head = 1
/\ tail' = 0
/\ pc' = (worker1 :> "casA" @@ worker2 :> "deq" @@ worker3 :> "deq")
/\ disk' = <<1>>
/\ head' = 2
/\ __trace_var_157369392033116000' = 42

...
  1. org.lamport.tla.toolbox.tool.tlc.launch.TraceExplorerDelegate.finalLaunchCheck(ILaunchConfiguration, String, IProgressMonitor) performs the following:

    1. Parses the set of modules from step (2.); if parsing errors are found, the launch is halted and the errors are presented to the user
    2. Runs level checking; if level 3 (Temporal) formulae are found, the launch is halted and the user is informed
    3. Write the trace files again with TraceExpressionModelWriter
  2. org.lamport.tla.toolbox.tool.tlc.launch.TraceExplorerDelegate.launch(ILaunchConfiguration, String, ILaunch, IProgressMonitor) performs the following:

    1. Spawns TLC such that it checks for deadlock; this forces it to print an error trace.

Reading error trace with trace expressions from TE.out into Toolbox's error view:

  1. org.lamport.tla.toolbox.tool.tlc.output.data.TraceExplorerDataProvider provides the following functionality:
    1. #getTraceExpressionsInformation() extracts the identifier for each trace expression from TE.tla
    2. #processTraceForTraceExplorer() merges the evaluated trace expressions into the original TLCError instances (via TLCError.apply(TLCError, Map<String, Formula>, HashTable<String, TraceExpressionInformationHolder>, String).) The new instances of TLCVariable which appear in each TLCState of the error instance are marked appropriately as being trace explorer expressions.
@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Nov 14, 2019

@quaeler Please review and add your own observations.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Nov 18, 2019

@alygin Would the user-experience described below be a fit for https://github.com/alygin/vscode-tlaplus?

@alygin

This comment has been minimized.

Copy link

@alygin alygin commented Nov 18, 2019

@lemmy, I totally like the idea of moving the trace evaluation feature to TLC and making it accessible to tools like the vscode extension.

As for the implementation details, the approach with a file that contains only expressions (two birds / one stone) seems the most viable to me. If such file exists (there must be some naming convention to detect it), the extension could display a link near the error trace which runs the expressions evaluation process and refreshes the error-trace-tree. That seems doable.

@lemmy lemmy added this to the 1.6.1 milestone Nov 18, 2019
@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Nov 20, 2019

@quaeler The patch below takes a stab at generating a more readable SpecTE.tla by generating sub-actions instead of a single next-state relation with multiple disjuncts. It needs polishing though.

TraceExpressionModelWriter.java.txt

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Dec 1, 2019

The implementation of this issue is taking place on the ldq-393-* branches off my fork and is following the following three-ish stage approach:

First stage (completed with 5286ead):

  • move common error / state / variable architecture into tlatools where possible.
  • move common writer architecture into tlatools where possible.
  • create new CL application, TraceExplorer, to be able to consume an existing MC.out in a normal model-check-ran directory and produce [what is referred to in this issue as] SpecTE.tla (and SpecTE.cfg) (if one does not exist; if one does exist it can be overwritten by specifying a force-overwrite flag, else the app execution halts.)

Second stage (completed with numerous commits ending in d9ed98c):

  • as part of all model checking, have TLC emit a SpecTE.tla (and SpecTE.cfg) in the the appropriate situations.
  • include the current MC.out content as a prefix to the module definition of SpecTE; consider renaming this file to be MC_out.tla.

Second stage bis (completed with 23f73b0):

  • change the contents of the second stage's model-check-tool-message-output-prefixed-SpecTE-TLA to be a single monolith TLA file which includes the dependent, non-StandardModules, modules.

Third stage (completed with ddcfd9a):

  • modify TraceExplorer to consume a list of expressions from a file specified via command line parameter (we don't want to automatically consume an appropriately named file in the working directory as that would preclude running TraceExplorer in different configurations.)
    • if a SpecTE.tla and SpecTE.cfg do not exist, the generation from the first stage above will be employed
    • this stage's functionality will create a [what is referred to in this issue as] TE.tla (and TE.cfg) file which includes appropriate conjunctions based on the expressions read from the file.
    • model checking will then be performed on the TE spec
    • lastly, a courtesy pretty-print will be done, featuring ANSI-bolding of the trace expressions

Fourth stage (current stage of implementation):

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Dec 1, 2019

Can parts of the functionality already be used? Does it make sense to deliver this to master incrementally?

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Dec 1, 2019

I think it makes sense to deliver the first stage to master when it's done and implement the subsequent stages on fresh branches.

As far as functionality, the first two bullet items don't really introduce functionality (it's largely pushing peas around the dinner plate.) The third bullet point is still in progress and seems atomic.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Dec 1, 2019

@alygin As the primary consumer of this feature, does this align with your release roadmap?

@alygin

This comment has been minimized.

Copy link

@alygin alygin commented Dec 2, 2019

@lemmy, it's totally ok. I think I'll ship v1.3 with the tla2tools.jar rev e25ead4 (the one with IDE name option) and then upgrade after the expr evaluation feature is implemented.

Though I need to change its displayed version somehow, the nightly build prints TLC2 Version 2.15 of Day Month 20??. What would be the easiest way to do that?


Version number discussion has been moved to issue #406 (comment)

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Dec 3, 2019

@quaeler Please keep an open eye if it's possible to also address the need for the common workaround below. I'd assume that passing trace expressions from the command-line would implementation-wise pretty close to it (I don't remember if we decided to support trace expression on the command-line though).

https://github.com/kelvich/tlaplus_jupyter/blob/50506379e1d63c251c4877c81b041698d089738e/tlaplus_jupyter/kernel.py#L228-L270

lemmy referenced this issue Dec 10, 2019
[Refactor][TLC]
@tlaplus tlaplus deleted a comment from alygin Dec 12, 2019
@tlaplus tlaplus deleted a comment from alygin Dec 12, 2019
quaeler added a commit to quaeler/tlaplus that referenced this issue Dec 20, 2019
. removed 'simple' versions of state and variable - introduced tlatools versions
. abstracted spec writer and a TE spec writer down to tlatools - Eclipse friendly subclasses preserved in toolbox
. MC out parser to create tlatools model objects for error, state, variable
. skeleton of TLC changes to glue this together
. clean up and consolidating of a lot of constant usage and oft-written in-line-strings into a tlatools constant class
. more architectural improvements to support new functionality
. further work on model check assets parsing for SpecTE generation
. most SpecTE writing code
. comments, clean-up
. work on recovering constants and definitions in forms which the spec writers expect
. architectural improvments and comments
. generation of a functioning SpecTE is now working - at least for the initial cases in which the original model checking was done against a SPECIFICATION behavior
. QC finished
. unit tests
quaeler added a commit to quaeler/tlaplus that referenced this issue Dec 20, 2019
. refactoring of spec writing and error-state-variable atoms into the tlatools level
. creation of a model check output parser to capture an error state list
. creation of the TraceExplorer command line application to:
.. generate SpecTE from the .tla/.cfg/.out triplet from a model checking run
.. pretty print to System.out the error state trace specified in an .out
. unit tests for the CFG and TLA copiers
. documentation

Issue tlaplus#393
[Feature][Tools][Toolbox]
quaeler added a commit that referenced this issue Dec 20, 2019
. refactoring of spec writing and error-state-variable atoms into the tlatools level
. creation of a model check output parser to capture an error state list
. creation of the TraceExplorer command line application to:
.. generate SpecTE from the .tla/.cfg/.out triplet from a model checking run
.. pretty print to System.out the error state trace specified in an .out
. unit tests for the CFG and TLA copiers
. documentation

Issue #393
[Feature][Tools][Toolbox]
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Dec 20, 2019

Stage 1 completed with 5286ead.

See the read-me concerning the command line application.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Dec 20, 2019

Minor improvements & observations:

  1. Instead of generic naming of sub-actions (i.e. next_1234567889), use the sub-actions name of the original spec (A_123456789, DoX_123456790) 75be65a
  2. Stable names for INIT and NEXT 75be65a
  3. Better error message when MC.out cannot be parsed because "-tool" markers are missing. 2cdc135"The output file had no tool messages; was TLC not run with the '-tool' option when producing it?"
  4. Support for _TETrace and _TEPosition (add sequence of records preamble to SpecTE.) fa45eb2
  5. Make piping work: java -cp /opt/TLA+Toolbox/tla2tools.jar tlc2.TLC -tool -simulate MC | java -cp /opt/TLA+Toolbox/tla2tools.jar tlc2.TraceExplorer -generateSpecTE -overwrite 1773ca0
  6. Highlight changed variables similar to how the TB does it.
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Dec 20, 2019

Sure - will roll into stage 2. I was reusing existing spec writing code in stage 1.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Dec 21, 2019

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 17, 2020

f2808bd introduces manpages like help text for TLC; i'll next apply this to TraceExplorer, then add a flag to TLC for non-monolith-creation.

Screen Shot 2020-02-17 at 1 23 06 PM

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 17, 2020

@quaeler Looks great!

quaeler added a commit to quaeler/tlaplus that referenced this issue Feb 18, 2020
. Making TraceExplorer use the new manpages-esque usage generator
. Improving the description markup regex in the usage generator

[Enhancement][Tools]
quaeler added a commit that referenced this issue Feb 18, 2020
. Making TraceExplorer use the new manpages-esque usage generator
. Improving the description markup regex in the usage generator

[Enhancement][Tools]
quaeler added a commit to quaeler/tlaplus that referenced this issue Feb 18, 2020
. Now providing an option to not include the module TLA+ code of all dependent modules in the generated SpecTE.tla file (-nomonolith)

[Enhancement][Tools]
quaeler added a commit that referenced this issue Feb 18, 2020
. Now providing an option to not include the module TLA+ code of all dependent modules in the generated SpecTE.tla file (-nomonolith)

[Enhancement][Tools]
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 18, 2020

@will62794 3894e23 now features an optional -nomonolith flag on TLC (use -h to read about it :- ) )

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 18, 2020

Is the new TLC help in sync with https://lamport.azurewebsites.net/tla/tlc-options.html?

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 18, 2020

HTML contains, but help doesn't:

  • -userFile

HTML contains, erroneously:

  • -bound

HTML does not contain:

  • -h
  • -generateSpecTE
  • -nomonolith

I'll add -userFile to TLC.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 18, 2020

Would it be difficult to pretty-print TLC's help on the web s.t. Lamport's page can link to it directly?

Isn't/shouldn't -nomonolith be a sub-parameter of -generateSpecTE?

quaeler added a commit to quaeler/tlaplus that referenced this issue Feb 18, 2020
. Adding help text for '-userFile'
. Removing comments referencing an argument '-bound' which is no (t| longer) implemented in the code

[Enhancement][Tools]
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 18, 2020

I suppose you could pipe the help display to a text file and then put it on either one of your GitHub served sites, or INRIA, and then have LL link to that?

-nomonolith is a sub-parameter in the sense that nothing is done with it if generate is not also specified; i'm not sure i've ever seen 'an optional parameter of an optional argument' before in use in the wild, but we could insist that the user put -nomonolith directly after -generateSpecTE, but that seems artificial / needless.

@quaeler quaeler closed this Feb 18, 2020
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 18, 2020

Sigh - wrong button.

@quaeler quaeler reopened this Feb 18, 2020
quaeler added a commit that referenced this issue Feb 18, 2020
. Adding help text for '-userFile'
. Removing comments referencing an argument '-bound' which is no (t| longer) implemented in the code

[Enhancement][Tools]
@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 18, 2020

-dump already has sub-parameters: ... -dump dot colorize,actionlabels,snapshots Model.dot .... -simulate has sub-params too: file= and num=.

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 18, 2020

Good to know - neither are documented as such.

I'll examine the code for those and add the help text as appropriate; and then move no-mono to copy that behavior.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 18, 2020

We haven't even started with documenting the various JVM system properties of TLC. :-p

quaeler added a commit to quaeler/tlaplus that referenced this issue Feb 19, 2020
. Clarified help text for dump and simulate to include sub-options
. Moved '-nomonolith' to a sub-option ('nomonolith') of '-generateSpecTe', ammended help text
. Improved Usage Generator to accept and display sub-options

[Enhancement][Tools]
quaeler added a commit that referenced this issue Feb 19, 2020
. Clarified help text for dump and simulate to include sub-options
. Moved '-nomonolith' to a sub-option ('nomonolith') of '-generateSpecTe', ammended help text
. Improved Usage Generator to accept and display sub-options

[Enhancement][Tools]
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 19, 2020

-dump and -simulate help texts updated concerning sub-options and nomonolith moved to be a sub-option to -generateSpecTE with 97b2949

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 19, 2020

JVM_ARGUMENTS.add("-XX:MaxDirectMemorySize=5120m");
JVM_ARGUMENTS.add("-Xmx2560m");
JVM_ARGUMENTS.add("-XX:+UseParallelGC");
JVM_ARGUMENTS.add("-Dfile.encoding=UTF-8");
JVM_ARGUMENTS.add("-Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet");
should neither set MaxDirectMemorySize nor use tlc2.tool.fp.OffHeapDiskFPSet. Instead, trace exploration should use tlc2.tool.fp.FPSetFactory.getImplementationDefault(). Also, why does it set Xmx2560m?

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 19, 2020

It sets something larger than the default 1GB size because 1GB as a general size seems too small, no? I'm open to alternate ways to have the user specify what they think the runner's max heap should be.

Will remove MaxDirectMemorySize, and set the .impl to be FPSetFactory.getImplementationDefault()'s return value.

@lemmy

This comment has been minimized.

Copy link
Member Author

@lemmy lemmy commented Feb 19, 2020

How many states do you expect TLC to generate during trace exploration?

@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 19, 2020

:- ) true, but there's something which feels starving in giving it the default. I'll give them an optional JVM argument specification in the same way they have one for TLC arguments.

quaeler added a commit to quaeler/tlaplus that referenced this issue Feb 19, 2020
. Removed Xmx and XX:MaxDirectMemorySize for TLCRunner's default JVM arguments
. Added a optional parameter to TraceExplorer's -traceExpressions and -replBis to allow the user to pass JVM arguments to the runner
. Conformed TraceExplorer's valued parameters to be separated by a space and not an equals sign
. Ceased redundant "Error: Error:" log prefix

[Enhancement][Tools]
quaeler added a commit that referenced this issue Feb 19, 2020
. Removed Xmx and XX:MaxDirectMemorySize for TLCRunner's default JVM arguments
. Added a optional parameter to TraceExplorer's -traceExpressions and -replBis to allow the user to pass JVM arguments to the runner
. Conformed TraceExplorer's valued parameters to be separated by a space and not an equals sign
. Ceased redundant "Error: Error:" log prefix

[Enhancement][Tools]
@quaeler

This comment has been minimized.

Copy link
Collaborator

@quaeler quaeler commented Feb 19, 2020

TLCRunner JVM arguments addressed with 57603d9

@lemmy lemmy mentioned this issue Feb 25, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
ldq
Awaiting triage
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
4 participants
You can’t perform that action at this time.