Как создать статическую модель состояния в Alloy?

Question

У меня есть две «Системы», обозначающие System1 и System2. Я хочу, чтобы каждая система имела состояние из конечного числа состояний (точнее, On или Off). Я также хочу, чтобы System1 мог изменять состояние System2 с On на * 1008. *. Я изо всех сил пытаюсь понять, где я должен использовать предикаты, функции и что я должен назначить полям? Я нашел информацию о динамических моделях, но я не хочу вводить время. Как мне смоделировать, что System1 может переключать состояние System2?

Большое спасибо

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{}

Answer 1

Если вы хотите смоделировать идею о том, что System2 (например) имеет изменяющееся состояние, это означает, что вам нужно каким-то образом представлять разные состояния в разное время. Поэтому некоторое представление о времени или состоянии неизбежно.