Get model checker to spit out full state trace on failed assertion?

[Andrew Helwer]

I specified the Die Hard problem in Runway. The problem, if you're unaware, is to get 4 gallons of water given only 5 gallon and 3 gallon jugs. It was famously featured in Die Hard 3 (scene) and is a good introductory specification problem. You set up the rules of the system then assert as an invariant that you'll never have 4 gallons of water; when this fails, the model checker spits out the steps to solve the problem.

My spec (see source here) apparently works just fine, but the model checker only spits out the last state transition rather than all of them:

C:\Users\ahelwer\Source\GitHub\runway-compiler>node --harmony .\bin\main.js chec
k ..\runway-tla-eval\DieHard.model
Was at {
  "jugs": [
    [
      1,
      {
        "volume": 5,
        "currentLevel": 5
      }
    ],
    [
      2,
      {
        "volume": 3,
        "currentLevel": 2
      }
    ]
  ]
}
Applied transfer(2)
Reached {
  "jugs": [
    [
      1,
      {
        "volume": 5,
        "currentLevel": 4
      }
    ],
    [
      2,
      {
        "volume": 3,
        "currentLevel": 3
      }
    ]
  ]
}
Failed Success
C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\modelchecker.js:112
              throw e;
              ^

ModelingAssertionError: Assertion failed: !=(jug.currentLevel, 4) at ..\runway-t
la-eval\DieHard.model: line 71, col NaN to line 71, col NaN
    at Base (C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\errors.js:15:10)

    at Runtime (C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\errors.js:57:
10)
    at Assertion (C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\errors.js:9
2:10)
    at Assert.execute (C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\statem
ents\assert.js:33:13)
    at C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\statements\sequence.js
:21:38
    at Array.forEach (native)
    at Sequence.execute (C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\stat
ements\sequence.js:21:21)
    at Block.execute (C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\stateme
nts\block.js:28:16)
    at C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\statements\foreach.js:
63:21
    at C:\Users\ahelwer\Source\GitHub\runway-compiler\lib\types\array.js:47:34

Is there a way to get the full state transition sequence? Thanks!

[Diego Ongaro]

That's funny. I hadn't seen it before. I don't know how that's a good problem for a Hollywood movie, though; it seems more appropriate for The Amazing Race.

There's no flag on the model checker now to print out/save the whole execution, but there ought to be. Want to create an issue to track it? https://github.com/salesforce/runway-compiler/issues

Cheers,

Diego

--
You received this message because you are subscribed to the Google Groups "runway-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to runway-dev+...@googlegroups.com.
To post to this group, send email to runwa...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/runway-dev/e2767e51-2a12-4024-8195-0937bc6d30e3%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Andrew Helwer]

Done! https://github.com/salesforce/runway-compiler/issues/7