Questions about runway modeling check

[yn...@ucsc.edu]

Hi,

I have a few questions about runway modeling check: 

1. there are many model checking method. what is runway based on? Could you give me a reference?

2. I've used the model checker to check the "toomanybananas" model. No bug is reported. is that normal?  I mean, the "toomanybananas" model certainly have some problems.

[Diego Ongaro]

On Fri, Oct 28, 2016 at 2:49 PM, <yn...@ucsc.edu> wrote:

Hi,

I have a few questions about runway modeling check: 

1. there are many model checking method. what is runway based on? Could you give me a reference?

It's a brute force BFS at the moment. This isn't efficient, but we have to start somewhere. The main loop is https://github.com/salesforce/runway-compiler/blob/42fc416/lib/modelchecker.js#L87. It'd be great to replace this with something more efficient eventually, probably by compiling down to an external model checker.

 

2. I've used the model checker to check the "toomanybananas" model. No bug is reported. is that normal?  I mean, the "toomanybananas" model certainly have some problems.

The model checker doesn't play well with random numbers. There's more detail here: https://github.com/salesforce/runway-compiler/issues/2

 

--
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+unsubscribe@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/7a129685-1790-4252-b55d-97488c1ea364%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[yn...@ucsc.edu]

 I've replaced the random number on "toomanybananas" model with a constant.  Still, the model checker didn't report any bug.  

On Friday, October 28, 2016 at 3:03:23 PM UTC-7, Diego Ongaro wrote:

On Fri, Oct 28, 2016 at 2:49 PM, <yn...@ucsc.edu> wrote:

Hi,

I have a few questions about runway modeling check: 

1. there are many model checking method. what is runway based on? Could you give me a reference?

It's a brute force BFS at the moment. This isn't efficient, but we have to start somewhere. The main loop is https://github.com/salesforce/runway-compiler/blob/42fc416/lib/modelchecker.js#L87. It'd be great to replace this with something more efficient eventually, probably by compiling down to an external model checker.

 

2. I've used the model checker to check the "toomanybananas" model. No bug is reported. is that normal?  I mean, the "toomanybananas" model certainly have some problems.

The model checker doesn't play well with random numbers. There's more detail here: https://github.com/salesforce/runway-compiler/issues/2

 

--
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.

[Diego Ongaro]

Are you perhaps running the version of the model where the people post a note on the house to prevent races? When I run toomanybananas/broken.model with the random number replaced, I see an error right away:

~/runway/compiler:master$ git show --oneline -s
42fc416 Prevent keywords and identifiers from jamming together
~/runway/compiler:master$ cat toomanybananas-broken.model 
/*
 * Copyright (c) 2016, Salesforce.com, Inc.
 * All rights reserved.
 * Licensed under the MIT license.
 * For full license text, see LICENSE.md file in the repo root or
 * https://opensource.org/licenses/MIT
 */

var bananas : 0..100 = 2;
type Person : either {
  Happy,
  Hungry,
  GoingToStore,
  ReturningFromStore {
    carrying: 0..8
  }
};
var roommates: Array<Person>[1..5];

rule step for state in roommates {
  match state {
    Happy {
      state = Hungry;
    }

    Hungry {
      if bananas == 0 {
        state = GoingToStore;
      } else {
        bananas -= 1;
        state = Happy;
      }
    }

    GoingToStore {
      state = ReturningFromStore {
        carrying: 3,
      };
    }

    ReturningFromStore(bag) {
      bananas += bag.carrying;
      state = Hungry;
    }
  }
}

invariant BananaLimit {
  assert bananas <= 8;
}
~/runway/compiler:master$ time ./bin/main.js check toomanybananas-broken.model 2>&1 | tail -n 20
      "Happy"
    ]
  ]
}
Failed BananaLimit
/Users/dongaro/runway/compiler/lib/modelchecker.js:112
              throw e;
              ^

ModelingAssertionError: Assertion failed: <=(bananas, 8) at toomanybananas-broken.model: line 49, col 3 to line 50, col 1
    at Base (/Users/dongaro/runway/compiler/lib/errors.js:14:24)
    at Runtime (/Users/dongaro/runway/compiler/lib/errors.js:56:24)
    at Assertion (/Users/dongaro/runway/compiler/lib/errors.js:91:24)
    at Assert.execute (/Users/dongaro/runway/compiler/lib/statements/assert.js:33:13)
    at /Users/dongaro/runway/compiler/lib/statements/sequence.js:21:38
    at Array.forEach (native)
    at Sequence.execute (/Users/dongaro/runway/compiler/lib/statements/sequence.js:21:21)
    at Block.execute (/Users/dongaro/runway/compiler/lib/statements/block.js:28:16)
    at Invariant.check (/Users/dongaro/runway/compiler/lib/statements/invariant.js:30:16)
    at /Users/dongaro/runway/compiler/lib/modelchecker.js:106:25

real 0m1.625s
user 0m0.956s
sys 0m0.144s