Licence | Master branch | Dev branch |
---|---|---|
-
OCaml 4.07.0 or later (tested with 4.07.0)
-
OPAM packages
xml-light
,ocamlfind
, andocamlbuild
(hint:opam install <package name>
) -
Python 2.7
-
Java runtime version 8 (tested with Java SE Development Kit 8u181).
-
Graphviz (hint:
brew install graphviz
) -
Apache Ant, for building Alloy (hint:
brew install ant
)
-
Modify
configure.sh
to suit your OS. -
Run
source configure.sh
. -
Run
make install
. HTML documentation can now be browsed atdoc/index.html
. -
Run
make quicktest
. After a few minutes you should find some pictures of distinguishing executions in thepng
directory.
-
Each
.cat
file must begin with a description of the architecture being modelled. This must be one of:"BASIC"
,"C"
,"HW"
,"X86"
,"PPC"
,"ARM7"
,"ARM8"
,"PTX"
,"OpenCL"
, or"OCaml"
. -
A reasonable fragment of the
.cat
language is supported.-
You can define sets and relations via
let x = e
. Names of sets must begin with an uppercase letter, and names of relations must begin with a lowercase letter. -
You can define functions via
let f(r1,...,rn) = e
. The name of the function must begin with an uppercase letter if the function returns a set, and must begin with a lowercase letter if the function returns a relation. Functions cannot return functions. Set-valued parameters must have a name beginning with an uppercase letter, and relation-valued parameters must begin with a lowercase letter. Parameters cannot be functions themselves. -
You can define relations (but not sets) recursively via
let x1 = e1 and ... and xn = en
, and these are unrolled a fixed number of times when translating into Alloy (since Alloy only checks up to a finite bound anyway). The number of unrollings is set by the-u
flag, which defaults to 3. -
You can define a consistency axiom of the model called
name
viaacyclic|irreflexive|empty e as name
. You can define a 'definedness' axiom (i.e., one that must hold of every consistent execution or else the whole program is undefined) by prepending the statement above withundefined_unless
, and you can define a 'deadness' axiom (i.e., one that must hold of an inconsistent execution in order to guarantee that the resultant litmus test has no other passing executions) by prepending the statement above withdeadness_requires
instead. -
You can include the definitions and axioms of the
submodel.cat
file viainclude submodel.cat
.
-
-
There are a few syntactic restrictions on
.cat
files.-
The variable
int
, built into Herd, clashes with a keyword in Alloy, so is not allowed. You can usethd
instead. -
The variable
X
, built into Herd, clashes with another variable in Alloy, so is not allowed. You can usedomain(atom) | range(atom)
instead. -
The variables
L
andA
are used in Herd for 'release' and 'acquire' accesses in the Arm8 architecture, but these clash with the variables for 'local' accesses in OpenCL and 'atomic' accesses in C and OpenCL, respectively. Alloy does not allow variables to be re-used in this way, so you must useSCREL
andSCACQ
in the Arm8 architecture instead.
-