Skip to content
Permalink
Branch: master
Commits on Oct 18, 2019
  1. Performance bottleneck creating the profiler tree (CostModel) with large

    lemmy committed Oct 17, 2019
    specs.
    
    [Bug][TLC]
  2. Correctly handle function definitions with nested LETIN statements

    lemmy committed Oct 16, 2019
    when constructing the profiler tree.
    
    Symptom is that TLC reports the following:
    
    CostModel lookup failed for expression <loc A>. Reporting costs into
    <locB>
    
    [Bug][TLC]
  3. Support launching TLC from a relative path.

    lemmy committed Oct 17, 2019
    As a side effect, TLC will create the states/ directory in the CWD.
    
    This is incomplete in that it has only been tested for BFS mode but not
    for DFS, simulation, or checkfile.
    
    [Bug][TLC]
Commits on Oct 17, 2019
  1. Deleting a spec that has unsaved changes - #375

    quaeler committed Oct 17, 2019
    - Fix for the issue, and changelog verbiage documenting the fix.
    
    #375
    [Bug][Toolbox]
  2. See d784869

    lemmy committed Oct 17, 2019
    [Bug][TLC]
  3. Correctly handle OTHER branch of CASE statements when constructing the

    lemmy committed Oct 17, 2019
    profiler tree.
    
    Symptom is that TLC reports the following:
    
    CostModel lookup failed for expression <loc A>. Reporting costs into
    <locB>
    
    [Bug][TLC]
  4. Correctly handle (recursive) function definitions when constructing the

    lemmy committed Oct 16, 2019
    profiler tree.
    
    Symptom is that TLC reports the following:
    
    CostModel lookup failed for expression <loc A>. Reporting costs into
    <locB>
    
    [Bug][TLC]
Commits on Oct 16, 2019
  1. NullPointerException when profiling actions with nested LET/IN

    lemmy committed Oct 16, 2019
    expression.
    
    Fixes GitHub issue #377
    #377
    
    [Bug][TLC]
  2. Make it extra clear that esc are shared publicly on the web.

    lemmy committed Aug 23, 2019
    [Feature][Toolbox]
  3. New model shows single page - #281

    quaeler committed Oct 16, 2019
    - Changelog and help text updating for this issue.
    
    #281
    [Feature][Toolbox]
Commits on Oct 14, 2019
  1. Refactor RCPTT scripts - #376

    quaeler committed Oct 14, 2019
    - Homogenized the usage of constants.
    - Expanded the constants to include common text for tabs, sections, links, dialog, button, views, and menu paths.
    - Remove redundant enablement checks in favor of doing it in one test out of the 58.
    - Similarly, the "typing" of a spec is now done in one test; all other tests use the much faster 'set-text' of spec text.
    - Quoted all text values (text, non-constant label and button names, etc.) in scripts.
    - Homogenized formatting.
    - Got rid of the uselss checks of 'find the UI element with the text "Bla" and then verify that it has the text "Bla".'
    - Condensed neighboring identical gets into 'with' blocks where noticed.
    
    #376
    [Feature][Toolbox]
Commits on Oct 12, 2019
  1. Error-Trace shows bogus values - #372

    quaeler committed Oct 12, 2019
    - Introducing an RCPTT which tests for this kind of regression.
    - Making the formatting of names of functional tests homogenous.
    
    #372
    [Bug][Regression][Toolbox]
  2. New model shows single page - #281

    quaeler committed Oct 12, 2019
    - Now a new model is display with only the Model Overview tab in view; the results page shows, as before, on execution of model checking, however there is also a hyperlink to open it for people interested in doing the evaluation of constant expressions (until some future day in which there is a REPL available.)
    - Other things encountered along the way, which resulted in code changes in this commit:
      - The main model page was written in such a way so as to cause an infinite loop during load should there be no other tabs (because the editor site in only given a functional selection provider in the results page.)
      - I refactored another inner enum class which was giving the Eclipse IDE syntax parser fits resulting in, for example, the editor for the ResultPage class ceasing to index / colorize / etc.
      - As i came across usages of the "m_" prefix i introduced, i undid them as able.
    
    #281
    [Feature][Toolbox]
Commits on Oct 8, 2019
  1. macOS machine setup is too unstable to be useful.

    lemmy committed Oct 8, 2019
    [Build]
Commits on Oct 6, 2019
  1. Some refactoring concerning model state change listeners; also haltin…

    quaeler committed Oct 6, 2019
    …g the "m_" prefix used in some of the refactored classes.
Commits on Oct 5, 2019
  1. Help windows should not float at modal level - #290

    quaeler committed Oct 5, 2019
    - Rearchitected the help display so that a window is no longer global and no longer displayed always above the main application window.
    
    #290
    [Feature][Toolbox]
  2. Error-Trace shows bogus values - #372

    quaeler committed Oct 5, 2019
    - Part of the underlying Tree implementation is relying on the item's hashcode, so our purposing of the hash calculations to make it easy to filter all TLCVariables based on a single proto-variable instance was resulting in the data for one instance of TLCVariable being shown for all of the same name/is-explorer couplet value. Have discontinued overriding hashcode for our filtering purposes.
    
    #372
    [Bug][Regression][Toolbox]
Commits on Oct 4, 2019
  1. TLCModelLaunchDataProvider's zero coverage never resets - #323

    quaeler committed Oct 4, 2019
    - Zero coverage is now reset between runs; architectural notes left in comments.
    
    #323
    [Bug][[Toolbox]
Commits on Oct 3, 2019
  1. First/Left-most item in profiler legend has bogus color.

    lemmy committed Oct 3, 2019
    [Bug][Toolbox]
Commits on Oct 2, 2019
  1. Addressing the issueWarn when PlusCal and TLA+ transpilation diverge -

    quaeler committed Oct 2, 2019
    …#296
    
    - When launching a model in which divergence existed and the model was dirty, the user would be double-warned; they are now only warned once per launch in this scenario.
    
    #296
    [Feature][[Toolbox]
  2. Teasing out the concatenated menu into nested blocks in the hope that…

    quaeler committed Oct 2, 2019
    … this will shed some light on which part of the concatenation is failing with macOS build test.
  3. Sign macOS Toolbox releases again.

    lemmy committed Oct 2, 2019
    [Build]
  4. Unless TLC's exit value is 1 or 255 (see EC.java), run the shutdown

    lemmy committed Oct 2, 2019
    sequence.
    
    In other words, ignore all non-zero exit values because the represent
    regular termination in which case we can safely terminate the cloud
    instance.
    
    See commit 2b15549
    
    [Bug][Toolbox]
Commits on Oct 1, 2019
  1. Copy library modules to CloudTLC if any.

    lemmy committed Oct 1, 2019
    CloudTLC deploys a custom packaged tla2tools.jar on the remote instance,
    which is self-contained. I.e. it contains all of the spec's dependencies
    such as modules from the library path and TLC module overrides. Here we
    make sure these dependencies get included in the custom tla2tools.jar
    (see PayloadHelper) by copying them to the model directory.
    
    [Feature][Toolbox]
  2. Refactor how the TLC job mode gets determined.

    lemmy committed Oct 1, 2019
    [Refactor][Toolbox]
  3. Open the ModelEditor on the CloudTLC snapshot after instance

    lemmy committed Sep 30, 2019
    provisioning has finished.
    
    The output/result of the (remote) CloudTLC run is *not* reported into
    Model_1 but into its most recent snapshots. Without opening the
    ModelEditor on the snapshot, it appears as if nothing is happening
    (unless the TLCConsole happens to be open).
    
    [Feature][Toolbox]
  4. Refactor model.getSpec() into variable.

    lemmy committed Sep 30, 2019
    [Refactor][Toolbox]
  5. Support editor folding of TLA+ translation of PlusCal algorithm - #329

    quaeler committed Oct 1, 2019
    - The PlusCal template now generates a closing comment line which obeys our stated rule about closing comment lines (only 1-N asterisk followed by a right paren.)
    - The closing comment line searched for by the folding reconciler now accepts a line generated by older templates - specifically potentially a space in column 1, followed by 1-N asterisk (followed by a right paren.)
    
    #329
    [Feature][Toolbox]
  6. Warn when PlusCal and TLA+ transpilation diverge - #296

    quaeler committed Oct 1, 2019
    - When 'Explore'ing an error trace expression against a spec which has a PlusCal state which would generate a dialog notification to the user, the message dialog was being invoked on a non-SWT thread. Addressing that problem.
    
    #296
    [Feature][[Toolbox]
Commits on Sep 26, 2019
  1. Remove finite sub-sequences of stuttering from simulation mode

    lemmy committed Sep 25, 2019
    error-trace.
    
    [Feature][TLC]
  2. When a MethodValue throws an exception during evaluation whose message

    lemmy committed Sep 26, 2019
    is null, TLC returns a useless error message.
    
    [Feature][TLC]
  3. Store if a module has been loaded from a library path.

    lemmy committed Sep 25, 2019
    Instead of trying to infer if a module has been loaded from a library
    path in higher layers of TLC and the Toolbox (which leads to subtle bugs
    when wrong), remember the location that a module was loaded from.
    
    I believe the following methods could be refactored similarly but I'm
    worried it will break things in subtle ways:
    util.FilenameToStream.isStandardModule(String)
    tla2sany.semantic.SemanticNode.isStandardModule()
    tla2sany.semantic.ModuleNode.isStandard()
    
    (in combination with
    tla2sany.semantic.StandardModules.isDefinedInStandardModule)
    
    [Refactor][TLC]
Commits on Sep 25, 2019
  1. Start TLC from specific error trace frame - #275

    quaeler committed Sep 25, 2019
    - Removing long tool tip text, placing it in the initial variable viewer text area.
    - Introducing the ability to get a conjuctive description of a TLCState with or without trace expressions
    - The state is now either substituted as the model checker's INIT state or appended with a conjunction to a pre-existing temproral specification, depending on the previously defined behavioral specification type.
    
    Issue #275
    [Feature][Toolbox]
Commits on Sep 24, 2019
  1. Print action names in error-trace of simulation mode.

    lemmy committed Sep 24, 2019
    [TLC][Feature][Changelog]
Older
You can’t perform that action at this time.