Can someone help with my alloy code, I've developed an Alloy model for a smart home energy system, which includes signatures for rooms, appliances, sensors$,$ and systems, as well as enums for sensor types, appliance statuses, and temperature ranges. I've also defined functions for calculating average temperature and safety$/$liveness properties. I am trying to generate some instances but I am bust. Here is what I have so far. module SmartHomeEnergySystem

$//$ Import relational utility modules

open util$/$relation

$//---$ Signatures $---$

sig Room $\{$

sensors: set Sensor,

appliances: set Appliance,

temperature: TempRange,

lighting: LightingLevel

$\}$

sig Sensor $\{$

type: SensorType,

readings: seq Int

$\}$

sig Appliance $\{$

status: ApplianceStatus,

energyUse: Int

$\}$

sig System $\{$

rooms: set Room,

userPreferences: UserPreferences,

currentState: State,

transitions: set Transition $//$ Defines possible transitions

$\}$

sig Transition $\{$

fromState: State,

toState: State

$\}$

sig UserPreferences $\{$

preferredTemp: TempRange,

preferredLighting: LightingLevel

$\}$

enum SensorType $\{$ TEMPERATURE$\_$SENSOR, OCCUPANCY$\_$SENSOR, LIGHT$\_$SENSOR $\}$

enum ApplianceStatus $\{$ APPLIANCE$\_$ON$,$ APPLIANCE$\_$OFF, APPLIANCE$\_$STANDBY $\}$

enum TempRange $\{$ TEMP$\_$VERY$\_$LOW, TEMP$\_$LOW, TEMP$\_$MEDIUM, TEMP$\_$HIGH, TEMP$\_$VERY$\_$HIGH $\}$

enum LightingLevel $\{$ LIGHTING$\_$DIM, LIGHTING$\_$MEDIUM, LIGHTING$\_$BRIGHT $\}$

enum State $\{$ STATE$\_$STANDBY, STATE$\_$OCCUPIED, STATE$\_$MONITORING, STATE$\_$OPTIMISING $\}$

$//---$ Relations $---$

fact RoomConfiguration $\{$

all r: Room $|$ #r$.$sensors $>0$ and #r$.$appliances $>0$

$\}$

$//---$ Safety Properties $---$

fact SafetyProperties $\{$

all r: Room $|$ some s: r$.$sensors $|$ s$.$type $=$ TEMPERATURE$\_$SENSOR

no r: Room, a: r$.$appliances $|$ a$.$status $=$ APPLIANCE$\_$ON and a$.$energyUse $>1000$

all s: System $|$ lone s$.$currentState

$\}$

$//---$ Liveness Properties $---$

fact LivenessProperties $\{$

all s: System $|$ some t: s$.$transitions $|$ t$.$fromState $=$ s$.$currentState

$\}$

$//---$ Atomic Properties $---$

fact AtomicProperties $\{$

all s: System $|$ some r: s$.$rooms $|$ r$.$temperature $=$ s$.$userPreferences.preferredTemp

all s: System $|$ all r: s$.$rooms $|$ r$.$lighting $=$ s$.$userPreferences.preferredLighting

$\}$

$//---$ Protocol Simulation $---$

pred simulateStateChanges$[$s: System, t: Transition$]\{$

t$.$fromState $=$ s$.$currentState implies t$.$toState in $($STATE$\_$MONITORING $+$ STATE$\_$OPTIMISING $+$ STATE$\_$OCCUPIED$)$

t$.$toState $=$ STATE$\_$STANDBY implies no r: s$.$rooms $|$ some a: r$.$appliances $|$ a$.$status $!=$ APPLIANCE$\_$STANDBY

$\}$

$//---$ Assertions and Checks $---$

assert SafetyCheck $\{$

all s: System $|$ all r: s$.$rooms $|$ no a: r$.$appliances $|$ a$.$status $=$ APPLIANCE$\_$ON and a$.$energyUse $>1500$

$\}$

assert LivenessCheck $\{$

all s: System $|$ eventually always $($some r: s$.$rooms $|$ r$.$temperature $=$ TEMP$\_$MEDIUM$)$

$\}$

$//$ Run checks and simulations

check SafetyCheck for $20$ but $5$ System, $8$ Room

check LivenessCheck for $20$ but $5$ System, $8$ Room, $20$ steps

$//---$ Example of running a specific scenario $---$

run $\{$

some s: System $|$ s$.$currentState $=$ STATE$\_$OCCUPIED and some r: s$.$rooms $|$ r$.$lighting $=$ LIGHTING$\_$BRIGHT

$\}$ for $8$ Room, $2$ System