How to model a water level control example with Alloy6

Hello ! I read an article named Model-Based Security Analysis of a Water Treatment System . It models an example of water level control using an earlier version of alloy, but I don’t know how to modify it to make it work properly in alloy6. I would appreciate if some kind person would suggest something.

open util/ordering[Tick] // Create a total ordering of global ticks
sig Tick {}

/**Generic part of a system model **/
abstract sig PhysicalProcess {state: PhysicalState one -> Tick}
abstract sig Sensor {process: PhysicalProcess}
abstract sig Actuator {state: ActuatorState one -> Tick}
abstract sig PLC{
    sensors: set Sensor,  actuators: set Actuator, processes: set PhysicalProcess,
    //At every tick,PLC reads states information from its sensors and actuators
    reads : (Sensor + Actuator) -> (State one -> Tick)
sig Compromised in Sensor + Actuator {}//Some of the sensors and actuators are compromised

/**SWaT-specific part of the model **/
one sig On,Off extends ActuatorState {}
abstract sig LevelState extends PhysicalState {}//State of water level in a tank
one sig UF,LL,L2,L1,L,H,H1,H2,HH,OF extends LevelState {}//UF underflow,OF overflow
//SWaT components for Stage P1
one sig RawWaterTank extends PhysicalProcess {}
one sig LIT101 extends Sensor {} {process = RawWaterTank}
one sig P101,MV101 extends Actuator {}
one sig PLC1 extends PLC {}{
    sensors = LIT101 + FIT101 and 
    actuators = P101 + MV101 and 
    processes = RawWaterTank
//Describes how the state of the water tank changes given the status of actuators
pred transition_RawWaterTank[t, t' :Tick]{
    let pre = state.t,post = state.t' {
        MV101.pre= On and P101.pre =On implies =this.pre
        MV101.pre= On and P101.pre =Off implies =increaseLevel[this.pre]
        MV101.pre= Off and P101.pre =On implies =decreaseLevel[this.pre]
        MV101.pre= Off and P101.pre =Off implies =this.pre }}
//Describes how the state of MV101 changes given PLC1 sensor readings
pred transition_MV101[t , t': Tick]{
    let plc1readings =PLC1.reads.t,pre =state.t,post= state.t'{
        plc1reading [LIT101]=H implies =Off
        plc1readings [LIT101]=L implies =On
        else MV101.pre }}
fact CompromisedBehavior{
//Sensor reading matches the actual state of the physical process if sensor is not compromised
    all s: Sensor,p :PLC,t :Tick | s not in Compromised implies (p.reads.t)[s] = s.proces.(state.t)
    //Reading from the actuator matches its actual state if it is not compromised
    all a: Actuator,p: PLC,t: Tick | a not in Compromised implies (p.reads.t)[a] = a.state.t
    //MV101 follows expected state changes if it is not compromised
all t :Tick - last | let t'| MV101 not in Compromised implies transition_MV101[t,t']

/**Safety property**/
//True iff system detects overflow or unexpected level changes in the raw water tank
pred alarm_tankMonitor [t : Tick]{
    let t0= t.prev,readings =(PLC1.reads.t0),level=readings[LIT101],
    |(level'=HH) or //reading indicates that water is about to overflow
    (readings[MV101]=On and readings[P101]=On and level'!=level) or
    (readings[MV101]=On and readings[P101]=Off and level'!=increaseLevel[level]) or
    (readings[MV101]=Off and readings[P101]=On and level'!=decreaseLevel[level]) or
    (readings[MV101]=Off and readings[P101]=Off and level'!=level)}
//True iff water overflows and no alarm is triggered
pred unsafe[t: Tick] {RawWaterTank.state.t = OF and no alarm_tankMonitor[t.prevs]}
//pred unsafe[t: Tick] {RawWaterTank.state.t = OF }

//System should never reach an unsafe state
assert SystemIsSafe{ no t :Tick | unsafe [t]}

In any case, it won’t work properly as this is not the complete model (as stated in the paper, and as can be seen from the reference to an undefined State sig in the reads field). I don’ t know whether the full model is available: @eskang ?