@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 different 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:
  
    //To-Do
  
  }
@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;
  }
}
