Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
695
stars
124
forks
source link
Temporal Specification and Analysis (Electrum) #136
Enhances Alloy with the ability to write mutable models (var sigs and fields), specify dynamic properties (LTL with past), and verify such properties through alternative backends (SAT and SMV). A presentation of this extended Alloy is available at here.
This is a major pull request, with significant changes in:
the language: signatures/fields can be marked as variable; expressions can be primed; formulas can use past/future LTL operators; scopes can be assigned to trace lengths (including unbounded scopes for complete model checking)
the analyses: relies on an extended version of Kodkod which natively supports LTL with past and analysis through SAT or SMV (including complete model checking); new configuration options selected through menu; a decomposed parallel analysis strategy
the visualiser: instances are now navigable traces rather than single states; new iteration operations available (new init, new config, fork)
This extension is not expected to not break compatibility with previous Alloy models, other than on those using protected ops and keywords, whose analysis should result in the same experience. Packaged example models were updated accordingly.
One major issue is the migration of the Kodkod backend into a separate repository. One issue is that changes to Kodkod made locally at org.alloytools.alloy have not (yet) been propagated to that new backend since commits cannot be easily identified.
I've annotated changes with an [HASLab] tag to make them more evident during development. I'll also leave local comments in the PR for relevant changes.
Enhances Alloy with the ability to write mutable models (
varsigs and fields), specify dynamic properties (LTL with past), and verify such properties through alternative backends (SAT and SMV). A presentation of this extended Alloy is available at here.This is a major pull request, with significant changes in:
This extension is not expected to not break compatibility with previous Alloy models, other than on those using protected ops and keywords, whose analysis should result in the same experience. Packaged example models were updated accordingly.
One major issue is the migration of the Kodkod backend into a separate repository. One issue is that changes to Kodkod made locally at
org.alloytools.alloyhave not (yet) been propagated to that new backend since commits cannot be easily identified.I've annotated changes with an
[HASLab]tag to make them more evident during development. I'll also leave local comments in the PR for relevant changes.