Search code examples
alloy

How to create a static state model in Alloy?

I have two "Systems", denote System1 and System2. I want each system to have a state from a finite number of states (On or Off to be precise) I also want System1 to be able to change the state of System2 from On to Off. I am struggling to understand where I should use predicates, functions, and what I should assign to fields? I have found information on dynamic models, but I do not want to introduce time. How do I model that System1 can switch the state of System2?

Many thanks

abstract sig System{ state: states}
one sig System1 extends System{
switch: System2 -> states
}
one sig System2 extends System{}
abstract sig states{}
one sig On,Off extends states{}

run{}
Solution

  • If you want to model the idea that System2 (for example) has a state that changes, that means you will need to somehow represent different states at different times. So some notion of time or state is unavoidable.