xfsp [
] // xfsp
@FormalML< system , 1.0 >:

system< timed % and , owned: #STS % statemachine , instance: [ + ] > ThermostatSystem {
/*owned: [
	statemachine< #STS , owned: simple % start % state , instance: [ + ] > Thermostat
	statemachine< #STS , owned: simple % start % state , instance: [ + ] > Equipment
] // end owned*/

@property:
	var time< uinteger > $time;
	unsafe var time< uinteger > $delta;

@routine:
	macro #model routine clock#reset($0: transient clock< uinteger > _c_){
		&spec:clock#reset._c_ := 0;
	}
	macro #model routine clock#update($0: transient clock< uinteger > _c_){
		&spec:clock#update._c_ := (&spec:clock#update._c_ + &spec::ThermostatSystem.$delta);
	}
@composite:
	statemachine< #STS , owned: simple % start % state , instance: [ + ] > Thermostat {
	/*owned: [
		state< start > q0
		state q1
		state q2
		state q3
		state q4
		state q5
		state q6
		state q7
	] // end owned*/

	@property:
		const integer TMIN = 20;
		const integer TMAX = 25;
		type mode enum {
			HEATING,
			COOLING
		}
		var integer t;
		var integer y;
		var integer z;
		public port input sens(integer);
		public port input equip(integer);
		public port input error(integer);
		public port output screen(integer);
		public port output dt(integer);
		public port output test(integer);

	/*region: [
		state< start > q0
		state q1
		state q2
		state q3
		state q4
		state q5
		state q6
		state q7
	] // end region*/

	@composite:
		state< start > q0 {
			transition t1 --> spec::ThermostatSystem.Thermostat.q0 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t2 --> spec::ThermostatSystem.Thermostat.q0 {
				input &spec:Thermostat.equip(&spec:Thermostat.y);
			}
			transition t3 --> spec::ThermostatSystem.Thermostat.q1 {
				input &spec:Thermostat.sens(&spec:Thermostat.t);
			}
		/*transition< incoming >: [
				transition t1 : state< start > q0 --> q0;
				transition t2 : state< start > q0 --> q0;
				transition t13 : state q1 --> q0;
				transition t43 : state q4 --> q0;
				transition t73 : state q7 --> q0;
		] // end transition*/

		}

		state q1 {
			transition t11 --> spec::ThermostatSystem.Thermostat.q2 { |;|
				guard (&spec:Thermostat.t < &spec:Thermostat.TMIN);
				output &spec:Thermostat.screen(HEATING);
			}
			transition t12 --> spec::ThermostatSystem.Thermostat.q5 { |;|
				guard (&spec:Thermostat.t > &spec:Thermostat.TMAX);
				output &spec:Thermostat.screen(COOLING);
			}
			transition t13 --> spec::ThermostatSystem.Thermostat.q0 { |;|
				guard ((&spec:Thermostat.t >= &spec:Thermostat.TMIN) && (&spec:Thermostat.t <= &spec:Thermostat.TMAX));
				output &spec:Thermostat.screen(OFF);
			}
		/*transition< incoming >: [
				transition t3 : state< start > q0 --> q1;
		] // end transition*/

		}

		state q2 {
			transition t21 --> spec::ThermostatSystem.Thermostat.q2 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t22 --> spec::ThermostatSystem.Thermostat.q3 {
				output &spec:Thermostat.dt((&spec:Thermostat.TMIN - &spec:Thermostat.t));
			}
		/*transition< incoming >: [
				transition t11 : state q1 --> q2;
				transition t21 : state q2 --> q2;
				transition t44 : state q4 --> q2;
		] // end transition*/

		}

		state q3 {
			transition t31 --> spec::ThermostatSystem.Thermostat.q3 {
				input &spec:Thermostat.equip(&spec:Thermostat.y);
			}
			transition t32 --> spec::ThermostatSystem.Thermostat.q3 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t33 --> spec::ThermostatSystem.Thermostat.q4 {
				input &spec:Thermostat.sens(&spec:Thermostat.t);
			}
		/*transition< incoming >: [
				transition t22 : state q2 --> q3;
				transition t31 : state q3 --> q3;
				transition t32 : state q3 --> q3;
		] // end transition*/

		}

		state q4 {
			transition t41 --> spec::ThermostatSystem.Thermostat.q4 {
				input &spec:Thermostat.equip(&spec:Thermostat.y);
			}
			transition t42 --> spec::ThermostatSystem.Thermostat.q4 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t43 --> spec::ThermostatSystem.Thermostat.q0 { |;|
				guard (&spec:Thermostat.t >= &spec:Thermostat.TMIN);
				output &spec:Thermostat.dt(0);
			}
			transition t44 --> spec::ThermostatSystem.Thermostat.q2 {
				guard (&spec:Thermostat.t < &spec:Thermostat.TMIN);
			}
		/*transition< incoming >: [
				transition t33 : state q3 --> q4;
				transition t41 : state q4 --> q4;
				transition t42 : state q4 --> q4;
		] // end transition*/

		}

		state q5 {
			transition t51 --> spec::ThermostatSystem.Thermostat.q5 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t52 --> spec::ThermostatSystem.Thermostat.q6 {
				output &spec:Thermostat.dt((&spec:Thermostat.TMAX - &spec:Thermostat.t));
			}
		/*transition< incoming >: [
				transition t12 : state q1 --> q5;
				transition t51 : state q5 --> q5;
				transition t74 : state q7 --> q5;
		] // end transition*/

		}

		state q6 {
			transition t61 --> spec::ThermostatSystem.Thermostat.q6 {
				input &spec:Thermostat.equip(&spec:Thermostat.y);
			}
			transition t62 --> spec::ThermostatSystem.Thermostat.q6 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t63 --> spec::ThermostatSystem.Thermostat.q7 {
				input &spec:Thermostat.sens(&spec:Thermostat.t);
			}
		/*transition< incoming >: [
				transition t52 : state q5 --> q6;
				transition t61 : state q6 --> q6;
				transition t62 : state q6 --> q6;
		] // end transition*/

		}

		state q7 {
			transition t71 --> spec::ThermostatSystem.Thermostat.q7 {
				input &spec:Thermostat.equip(&spec:Thermostat.y);
			}
			transition t72 --> spec::ThermostatSystem.Thermostat.q7 {
				input &spec:Thermostat.error(&spec:Thermostat.z);
			}
			transition t73 --> spec::ThermostatSystem.Thermostat.q0 { |;|
				guard (&spec:Thermostat.t <= &spec:Thermostat.TMAX);
				output &spec:Thermostat.dt(0);
			}
			transition t74 --> spec::ThermostatSystem.Thermostat.q5 {
				guard (&spec:Thermostat.t > &spec:Thermostat.TMAX);
			}
		/*transition< incoming >: [
				transition t63 : state q6 --> q7;
				transition t71 : state q7 --> q7;
				transition t72 : state q7 --> q7;
		] // end transition*/

		}

	}

	statemachine< #STS , owned: simple % start % state , instance: [ + ] > Equipment {
	/*owned: [
		state< start > s0
		state s1
		state s2
		state s3
		state s4
	] // end owned*/

	@property:
		var integer x;
		var boolean isOn;
		public volatile var clock< integer > c = 0;
		public port input dt(integer);
		public port output equip(integer);
		public port output error(integer);
		public const integer TIMEOUT = 0;

	/*region: [
		state< start > s0
		state s1
		state s2
		state s3
		state s4
	] // end region*/

	@composite:
		state< start > s0 {
			transition e1 --> spec::ThermostatSystem.Equipment.s1 { |;|
				input &spec:Equipment.dt(&spec:Equipment.x);
				&spec:Equipment.c := 0;
			}
		/*transition< incoming >: [
				transition e11 : state s1 --> s0;
				transition e21 : state s2 --> s0;
				transition e31 : state s3 --> s0;
		] // end transition*/

		}

		state s1 {
			transition e11 --> spec::ThermostatSystem.Equipment.s0 { |;|
				guard (&spec:Equipment.x == 0);
				tguard (&spec:Equipment.c <= 2);
				&spec:Equipment.c := 0;
				output &spec:Equipment.equip(0);
				&spec:Equipment.isOn := false;
			}
			transition e12 --> spec::ThermostatSystem.Equipment.s2 { |;|
				guard (&spec:Equipment.x > 0);
				tguard (&spec:Equipment.c <= 2);
				&spec:Equipment.c := 0;
				&spec:Equipment.isOn := true;
			}
			transition e13 --> spec::ThermostatSystem.Equipment.s4 { |;|
				tguard (&spec:Equipment.c > 2);
				output &spec:Equipment.error(&spec:Equipment.TIMEOUT);
			}
			transition e14 --> spec::ThermostatSystem.Equipment.s3 { |;|
				guard (&spec:Equipment.x < 0);
				tguard (&spec:Equipment.c <= 2);
				&spec:Equipment.c := 0;
				&spec:Equipment.isOn := true;
			}
		/*transition< incoming >: [
				transition e1 : state< start > s0 --> s1;
		] // end transition*/

		}

		state s2 {
			transition e21 --> spec::ThermostatSystem.Equipment.s0 { |;|
			}
			transition e22 --> spec::ThermostatSystem.Equipment.s2 { |;|
				guard (&spec:Equipment.x > 0);
				tguard (&spec:Equipment.c <= 1);
				&spec:Equipment.c := 0;
				output &spec:Equipment.equip(4);
				&spec:Equipment.x := (&spec:Equipment.x - 4);
			}
			transition e23 --> spec::ThermostatSystem.Equipment.s4 { |;|
				tguard (&spec:Equipment.c > 1);
				output &spec:Equipment.error(&spec:Equipment.TIMEOUT);
			}
		/*transition< incoming >: [
				transition e12 : state s1 --> s2;
				transition e22 : state s2 --> s2;
		] // end transition*/

		}

		state s3 {
			transition e31 --> spec::ThermostatSystem.Equipment.s0 { |;|
			}
			transition e32 --> spec::ThermostatSystem.Equipment.s3 { |;|
				guard (&spec:Equipment.x < 0);
				tguard (&spec:Equipment.c <= 1);
				&spec:Equipment.c := 0;
				output &spec:Equipment.equip(-4);
				&spec:Equipment.x := (&spec:Equipment.x + 4);
			}
			transition e33 --> spec::ThermostatSystem.Equipment.s4 { |;|
				tguard (&spec:Equipment.c > 1);
				output &spec:Equipment.error(&spec:Equipment.TIMEOUT);
			}
		/*transition< incoming >: [
				transition e14 : state s1 --> s3;
				transition e32 : state s3 --> s3;
		] // end transition*/

		}

		state s4 {
			transition e41 --> spec::ThermostatSystem.Equipment.s4 {
				input &spec:Equipment.dt(&spec:Equipment.x);
			}
		/*transition< incoming >: [
				transition e13 : state s1 --> s4;
				transition e23 : state s2 --> s4;
				transition e33 : state s3 --> s4;
				transition e41 : state s4 --> s4;
		] // end transition*/

		}

	@moe:
		@create{
			inst:Equipment.c := 0;
		}

	}

@com:
	connector< env > _#connector#0 {
		input spec::ThermostatSystem.Thermostat.sens;
		output spec::ThermostatSystem.Thermostat.screen;
	}
	connector< rdv , unicast > _#connector#1 {
		output spec::ThermostatSystem.Thermostat.dt;
		input spec::ThermostatSystem.Equipment.dt;
	}
	connector< rdv , unicast > _#connector#2 {
		input spec::ThermostatSystem.Thermostat.error;
		output spec::ThermostatSystem.Equipment.error;
	}
	connector< rdv , unicast > _#connector#3 {
		output spec::ThermostatSystem.Equipment.equip;
		input spec::ThermostatSystem.Thermostat.equip;
	}

@moe:
	@init{ |§|
		&spec::ThermostatSystem.$time := 0;
		&spec::ThermostatSystem.$delta := 0;
	}
	@irun{ |§|
		newfresh(&spec::ThermostatSystem.$delta)
		tguard (&spec::ThermostatSystem.$delta > 0);
		&spec::ThermostatSystem.$time := (&spec::ThermostatSystem.$time + &spec::ThermostatSystem.$delta);
		&spec:Equipment.c := (&spec:Equipment.c + &spec::ThermostatSystem.$delta);
	}

}
