Written by Tiago Massoni Rohit Gheyi and Paulo Borba. Updated for Alloy 3.0 and converted to html by Robert Seater.
In the case:
sig A {}{#A=1}
the fact is translated roughly into
{all this:A | #this=1}
This fact will hold true if A is empty (which is not what we wanted to show). Rather, use facts tied to the signature:
sig A {}
fact AFact { #A=1 }
For facts about cardinality, you could also just declare an appropriate scope:
Sig A {}
run show for 3 but exactly 1 A
run show
is the same as
run show for 3
If you have a complicated formula, refactor it to make it simpler. You then need to make sure the formula represents the same constraint. For example:
all disj a1,a2: Account | a1 in Branch.account_set
&& a2 in Branch.account_set
changes to
all disj a1,a2:Account | a1 + a2 in Branch.account_set
Create an assertion to make sure the formulas are equivalent
assert checkFact {all disj a1,a2: Account | a1 in Branch.account_set
&& a2 in Branch.account_set
<=> all disj a1,a2:Account | a1 + a2 in Branch.account_set}
check checkFact
One of these statements is not like the others:
state.map + here->there
state.(map + here->there)
(state.map) + here->there
If you're not sure what you're getting, add parens (or check equivalence like we did for formula refactoring above). Extra parens can also improve readability -- if you weren't sure then don't assume someone else will be sure what it means.
Some cardinality, existence facts are better suited for the body of a function that will be run in order to find an instance. You can make the model structures more reusable by moving these constraints to a particular function.
fact {
some Account
#Branch = 1
}
Rather:
pred show() {
some Account
#Branch = 1
}
Ask yourself "Is this a fundamental rule about the world, or just something I want to hold in one example?".
For example, you can model a bank system containing branches and accounts, including relations that only make sense if we consider the whole system.
sig Bank {
branches: set Branch
accounts: set Account
location: accounts -> !branches
...
}
In this case, if you want to model a system of a single Bank, you may declare it a singleton:
one sig Bank {...}
Branch 1<------------------>* Account (in UML)
Question: How to model a relationship like this in Alloy?
The choices would include either chosing one class to contain one relation (Branch.account_set or Account.location) or adding both relations to the corresponding signatures (as it would be done in Java, for example). The best choice is to choose one side to add the relation, probably the one that will be used more often, and use the transpose relation for the other side. An additional relation would make the model more complex, and would demand more computational power for analysis.
This situation may arise when we want to check a property (e.g. whether an operation is valid) that needs some specific atoms to be generated by the analyzer.
For example consider checking the following operation in a bank branch:
pred addAccount (b,b':Branch,a:Account) {
a !in b.account_set
b'.account_set = b.account_set + a
}
We want to check whether this operation is valid...the analyzer will work fine if we take this approach:
a) new signatures, representing specific branches and a specific account:
one sig BRANCH1,BRANCH2 extends Branch {}
one sig JOHN_ACCOUNT extends Account {}
b) a fact constraining these singletons for our purpose:
fact relateBranches {
BRANCH2.account_set = BRANCH1.account_set + JOHN_ACCOUNT
JOHN_ACCOUNT !in BRANCH1.account_set
}
c) finally the assertion that checks the operation for these singletons:
assert addAccountWorks {
addAccount(BRANCH1, BRANCH2, JOHN_ACCOUNT)
}
Now we make sure that the analyzer will not find counterexamples that don't apply to our solution and check the operation properly.
Back to the quickstart guide.