Unbounded Scope

Questions
1

I’m working in Alloy 6, trying to implement a workflow language based on tokens moving around and being consumed/created.

I’m trying to define a scope for my system, shown below.

image
image949×26 2.38 KB

I was just wondering if it is possible to set the scope for the “token” to unbounded, or something along these lines? Setting the tokens higher seems to make the enumeration much much slower.

Tokens are the only var objects in my system, so it would be ideal to have the scope variable too.
Here is the signature to my Token variable:

var sig Token {
var pos: one StartEvent + Activity + SequenceFlow
}

2

Hi,
to be able to fully automate verification in a formal method, a trade off must be made. There aren’t that many solutions and the one chosen by Alloy has the following characteristics:

  • expressive language
  • fast analysis techniques
  • only works on “small” models, which is OK for scenario exploration and bug finding
  • rather small, bounded scopes must be specified for all signatures (only the time dimension can remain unbounded if you rely on the nuXmv solver, but it will usually be effective only when other signatures have a small bound).

Sometimes, we are tempted to use Alloy to model a DSL (which what you seem to be doing) but the analysis technique at work in Alloy is in my experience not well suited to implement a complex operational semantics (such as tokens moving in a workflow). Alloy is not really meant as a language to implement interpreters.

2 Likes