Dash extension to Alloy Analyzer

Experimental
1

We are excited to release our first version of support for Dash editing/translation/execution within the Alloy Analyzer version 6. You can find our fork of the Alloy code base at:

The default branch is ‘dash’ for our extension.

Dash extends the Alloy language with constructs for describing transition systems similar to Statecharts (hierarchical, concurrent, labelled states and transitions).

We’ve worked hard on the README.md file to hopefully answer most questions about how to use it, but we welcome your questions, issues, comments, and suggestions. Tamjid Hossain is currently working on this development so you can send email to both of us. We will be regularly updating the repo, so if you are using Dash, I suggest updating it with a ‘git pull’ regularly.

Dash is continuing to be developed by Tamjid to support parameterized concurrent states (e.g., a set of servers with the same behaviour).

We would love to hear feedback!

Nancy Day (nday@uwaterloo.ca)
Tamjid Hossain (t7hossain@uwaterloo.ca)

1 Like
2

Hi Nancy and Tamjid,

Looks very interesting, and a nice experiment in combining Alloy with Statecharts. I wonder if as your research progresses it might be possible to find a smaller extension of Alloy 6 that would support this, perhaps in combination with a modeling pattern?

Daniel

3

Hi Daniel,

Are you thinking of an extension that would allow one to describe transitions but perhaps not state hierarchy? And a modelling pattern could capture the state hierarchy to avoid cluttering the language when this is not necessary? We would have to think about whether we could refactor Dash along these lines.

Nancy