Add invariant contract language support

In order to support various use cases, we need to support the definition of contracts:

Dynamic contracts will be useful for:

• defining valid initial states in goals (used on start of the model checker)
• help testing of GuardedAction (used for testing that the GuardedActions are semantically correct)

Static contracts will be useful for:

• validating the user model (assets and links)
• validating standard conformance/requirements ... (mitre, iso, ...)

example:

contracts {
		// check dynamic
		dynamic contract itemAreInASingleLocation(item : Item, zone1 : Zone, zone2 : Zone)
			description = " "
			guard = (zone1.itemsInZone.contains(item) && zone2.itemsInZone.contains(item) ) implies  (zone1 == zone2)
			guard = ! (zone1.itemsInZone.contains(item) && zone2.itemsInZone.contains(item) &&  (zone1 != zone2) )
		}
		dynamic contract itemAreOwnedByASingle(item : Item, attacker1 : Attacker, attacker2 : Attacker)
			description = " "
			guard = (attacker1.ownedItems.contains(item) && attacker2.ownedItems.contains(item) ) implies (attacker1 == attacker2)
		}
		dynamic contract pickedItemAreInZoneOrOwned (item : Item, zone : Zone, attacker : Attacker) {
			guard = ! (attacker.ownedItems.contains(item) && zone.itemsInZone.contains(item))
		}
		
		static contract insideIsDifferentFromOutSide (access : Access) {
			guard = access.inside != access.outside
		} 
		static warning contract BadgeDoorMustHaveAkey( badgeDoor : BadgeDoor) {
		    annotations {
		       "mitre.ID" = "ISO27001"
		    }
		    guard = ! badgeDoor.keys.isEmpty
		}
	}