Alloy Syntax Stuff

All of this stuff is Alloy syntax stuff.

Composite Predicates (simplified BNF) – pretty obvious, just explaining standard syntax of predicates (BNF = grammar defining predicates)

Alloy (the software we use) has a ‘rich collection’ of quantifiers that can be used in predicates – all, some, no, one, lone. Lone is a shorthand for ‘no or one’.

Examples of (primitive) predicates

a not = b
a = b
a not >= b

In alloy, looking up b in set a, you do b[a], not a[b] as you might think. You can also use a.b, which makes more sense.

Examples of binary operators in Alloy

Product

a->b  // product; a has s & b has t iff a->b has st

If you had a set X = {0,1,2,3}:

X->X = {0->0, 0->1, 0->2, 0->3, 1->0....3->3}

Join

a.b  // join; (some e | a has se & b has et) iff a.b has st

Kinda like joining two relations using transitivity. For example if in set a you have {0->2} and in set b you have {2->3}:

a.b = {0->3}

Also if you have a relation d = {0->1, 2->4, 3->2, 2->3} then

2.d = {4, 3}
d.2 = {3}

I think that’s the right way round.

Override

a++b // override

Overrides anything in a that can be overridden by something in b, e.g:

d = {0->2, 2->3, 3->2, 3->5}
c = {0->1, 3->1}
d++c = {0->1, 2->3, 3->1}

Note that this overrides the 2 3->* relations because there is one in c, and they both get overriden by that single 3->1 in c.

There’s others:

a+b  // union
a&b  // intersection
a-b  // difference
a<:b // b restricted to a, throwaway anything that isn't a->\*
a:>b // a restricted to b, throwaway anything that isn't \*->b

Unary operators in Alloy

~a  // reverise; like a 'but' but all tuples are REVERSED.
\*a  // reflexive transitive closure. Recursive: \*a = iden+a+a.a+a.a.a+a.a.a.a....
^a  // (irreflexive) transitive closure. Recursive: ^a = a+a.a+a.a.a+....

So \*a is apply ‘a’ 0 or more times, ^a is apply ‘a’ 1 or more times.

Constants

univ  // all the singleton tuples in the current universe
none  // the empty relation
iden  // the relation of everything in the current universe
      // to itself

none is quite useful, probably wont use the others.

Declarations

Look in Alloy documentation. Doesn’t make much sense, but probably because I don’t understand enough of what Alloy does yet.

Signatures

I can tell these are important because I saw this in Alloy

These are how you introduce Atoms.

sig A{}   // a set of atoms. Visualiser will know them as A$0, A$1 and so on
sig B{r : A} // Same as above, but also introduce a relation between B and A. It is the relation 'for every B there is a single A'
one sig C{} // A set of atoms that declare exactly one thing. A scalar in other words.
sig D extends B{s : lone C} // Kinda like a subclass but not quite. A subset of B, and s is the relation 'for every D there is one or none C'
sig E extends B{t : some D} // Same as above but also E is related to one or more D.

There’s also sig X in Y but I missed that.

Abstract signatures and Enumerations

An abstract sig is something you can’t have members of directly. You then have to have sub signatures to start with. This is a way of having names for the members of the abstract sig. This was used in the river thing, where you had an abstract sig ‘Object’, and then farmer chicken fox and grain defined as objects.

Constraining signatures

Useful. Again we saw this in the river crossing example:

sig A{  // Field declarations
	x, y : b  // two relations A -> one B
}{ // Constraints
	not x=y // 
}

Named predicates and expressions

We often want to give names to predicates and functions. Pretty obvious: pred p [parameters]{Pred} fun f [parameters] : Expr // Returned Type { Expr } // Value of function

Jalada