****Alloy Hints & Tips******

1)Be careful with implicit facts. In the case:
sig A {}{#A=1}

the fact is translated into {all this:A | with this | #A=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 }


2)The default scope for commands is three(3) atoms, so:

run show for 3 = run show


3)Formula refactoring: if you have a complicated formula, you refactor it to make it simpler, then you need to 
make sure the formula represents the same constraint:
Ex: 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


4)Be careful with operator precedence
all a1,a2: Account | a1.number = a2.number => a1 = a2
Rather:
all a1,a2: Account | (a1.number = a2.number) => a1 = a2
In addition, it improves readability


5)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.
Ex: fact{
    some Account
    #Branch = 1
    }
Rather:
fun show(){
    some Account
    #Branch = 1
}


6)You can model a single system by creating a signature that represent the general system.
Ex: 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 static (singleton):
static sig Bank {...}
    
7) Meaning of disj,part,exh qualifiers
We have two signatures A and B, subsets (extend) of C

	a) sig C{}
	   disj A extends C{...}
	   disj B extends C{...}
	   OR
	   disj A,B extends C{...}
	   meaning: A & B = {}

	b) sig C{}
	   exh A,B extends C{...} (exh applies only to signatures on the same line)
	   meaning: A + B = C     

	c) sig C{}
	   part A,B extends C{...} (part applies only to signatures on the same line)
	   meaning: A & B = {} && A + B = C

8)Modeling Technique: association between two signatures (classes)
Ex: 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.

9)Modeling specific atoms in Alloy
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. 
Ex: Checking the following operation in a bank branch:

det fun addAccount (b,b':Branch,a:Account) {
	a !in b.account_set
	b'.account_set = b.account_set + a
}

or 

det fun Bank::addAccount(a:Account):Branch {
    a !in this.account_set
    result.account_set = this.account_set + a
}

We want to check whether this operation is valid...the analyzer will work fine if we take this approach:
new signatures, representing specific branches and a specific account:
static disj sig BRANCH1,BRANCH2 extends Branch {}
static disj sig JOHN_ACCOUNT extends Account {}

a fact constraining these singletons for our purpose:
fact relateBranches {
     BRANCH2.account_set = BRANCH1.account_set + JOHN_ACCOUNT
     JOHN_ACCOUNT !in BRANCH1.account_set
}
finally the assertion that checks the operation for these singletons:
assert addAccountWorks {
	BRANCH1..addAccount(JOHN_ACCOUNT) = BRANCH2
}
Now we make sure that the analyzer will not find counterexamples that don't apply to our solution and check the 
operation properly.


10) Always use det (deterministic) for operations (high-level functions of the system - use cases)