@xfsp< system , 1.0 >:

timed system< and > ThermostatSystem {
	
@machine:
  statemachine< or > Thermostat {
  
  @private: // group declaration

      //constants defining the temperature thresholds
      const var integer TMIN = 20;
      const var integer TMAX = 25;
      
      //constants defining the diffrent modes
      type mode enum { OFF, HEATING, COOLING} 
      // OFF --> 0
      // HEATING --> 1
      // COOLING --> 2


      var integer t;
      var integer y;
      var integer z;

  @public: // group declaration

    port input sens (integer);
    port input equip(integer);
    port input error(integer);


    port output screen (integer);
    port output dt (integer);
    port output test (integer);
	
   @region:
  
    state<start> q0 {
    
      transition t1 --> q0 {
		input error(z);
      }
	  transition t2 --> q0 {
		input equip(y);
      }
	  transition t3 --> q1 {
		input sens(t);
      }
    }
    
	state q1 {
    
      transition t11 --> q2 {
		guard (t < TMIN);
		output screen(HEATING);
      }
	  transition t12 --> q5 {
		guard (t > TMAX);
		output screen(COOLING);
      }
	  transition t13 --> q0 {
		guard (t >= TMIN && t <= TMAX);
		output screen(OFF);
      }
    }
	
	state q2 {
	
      transition t21 --> q2 {
		input error(z);
      }
	  transition t22 --> q3 {
		output dt(TMIN-t);
      }
    }
	
	state q3 {
	
      transition t31 --> q3 {
		input equip(y);
      }
	  transition t32 --> q3 {
		input error(z);
      }
	  transition t33 --> q4 {
		input sens(t);
      }
    }
	
	state q4 {
	
      transition t41 --> q4 {
		input equip(y);
      }
	  transition t42 --> q4 {
		input error(z);
      }
	  transition t43 --> q0 {
		guard(t >= TMIN);
		output dt(0);
      }
	  transition t44 --> q2 {
		guard(t < TMIN);
      }
    }
	
	state q5 {
	
      transition t51 --> q5 {
		input error(z);
      }
	  transition t52 --> q6 {
		output dt(TMAX-t);
      }
    }
	
	state q6 {
	
      transition t61 --> q6 {
		input equip(y);
      }
	  transition t62 --> q6 {
		input error(z);
      }
	  transition t63 --> q7 {
		input sens(t);
      }
    }
	
	state q7 {
	
      transition t71 --> q7 {
		input equip(y);
      }
	  transition t72 --> q7 {
		input error(z);
      }
	  transition t73 --> q0 {
		guard(t <= TMAX);
		output dt(0);
      }
	  transition t74 --> q5 {
		guard(t > TMAX);
      }
    }
  }  

  statemachine< or > Equipment {
  @private: // individual declaration
    var integer x;
	var boolean isOn;
  @public: // individual declaration
    var clock<integer> c; // clock
    port input dt(integer);
    port output equip(integer);
    port output error(integer);

    const var integer TIMEOUT = 0;

	
  @region:
    state<start> s0 {
		transition e1 --> s1 {
			input dt(x);
			c = 0;
		}
	}
    state s1 {
		transition e11 --> s0 {
			guard (x == 0);
			tguard (c <= 2);
			//reset(c);
			c = 0;
			output equip(0);
			isOn = false;
		}
		transition e12 --> s2 {
			guard (x > 0);
			tguard (c <= 2);
			//reset(c);
			c = 0;
			isOn = true;
		}
		transition e13 --> s4 {
			tguard (c > 2);
			output error(TIMEOUT);
		}
		transition e14 --> s3 {
			guard (x < 0);
			tguard (c <= 2);
			//reset(c);
			c = 0;
			isOn = true;
		}
		
	}
	state s2 {
		transition e21 --> s0 {
			//unobservable action
		}
		transition e22 --> s2 {
			guard (x > 0);
			tguard (c <= 1);
			//reset(c);
			c = 0;
			output equip(4);
			x = x - 4;
		}
		transition e23 --> s4 {
			tguard (c > 1);
			output error(TIMEOUT);
		}
	
    }
    state s3 {
		transition e31 --> s0 {
			//unobservable action
		}
		transition e32 --> s3 {
			guard (x < 0);
			tguard (c <= 1);
			//reset(c);
			c = 0;
			output equip(-4);
			x = x + 4;
		}
		transition e33 --> s4 {
			tguard (c > 1);
			output error(TIMEOUT);
		}
	
    }
    state s4 {
      transition e41 --> s4 {
        input dt(x);
      }
    }
  }
@com:
  // environment
  connect< env >{
    input Thermostat->sens;
    output Thermostat->screen;
  }
  connect< rdv>{
    output Thermostat->dt;
    input Equipment->dt;
  }
  connect< rdv >{
    input Thermostat->error;
    output Equipment->error;
  }
  connect< rdv>{
    output Equipment->equip;
    input Thermostat->equip;
  }
}
