<PROBLEM>


<SYMBOLS>
# Name : [Unknown|Known|Alias] (* Optional comment *) ;

  ZC12 : Known (* le train 12 est dans la zone commune *);
  ZC34 : Known (* le train 34 est dans la zone commune *);
  TT_Limit34 : Known (* l'aiguillage est positionné pour le train 34 *);
  TT_Limit12 : Known (* l'aiguillage est positionné pour le train 12 *);
  XR12 : Known (* le train 12 arrive devant le feu de signalisation (voie 1)*);
  XR34 : Known (* le train 34 arrive devant le feu de signalisation (voie 3)*);
  XR43 : Known (* le train 34 arrive devant le feu de signalisation (voie 4)*);
  XR21 : Known (* le train 12 arrive devant le feu de signalisation (voie 2)*);
  
  T_Turn : Unknown (* positionner l'aiguillage vers 12 (monostable, position 34 par défaut) *);    
  FV12 : Unknown (* Allumer en vert feux 12 *);  
  FV34 : Unknown (* Allumer en vert feux 34 *);  
  FR12 : Unknown (* Allumer en rouge feux 12 *);  
  FR34 : Unknown (* Allumer en rouge feux 34 *);  
  
  AUT12 : Unknown (* Autoriser train 12, variable interne pour la SA *);  
  AUT34 : Unknown (* Autoriser train 34, variable interne pour la SA *);  
  
  
  
</SYMBOLS>
<ALIASES>
# Name = BooleanFormula (* Optional comment *) ;
</ALIASES>

<REQUIREMENTS>
# Name : BooleanFormula [=<|=] BooleanFormula (* Optional comment *) ;

RR10 : (* les 2 feux 12 sont exclusivement verts ou rouges *) 
FV12 = /FR12; 

RR11 : (* les 2 feux 34 sont exclusivement verts ou rouges *)
FV34 = /FR34;

RR12 : (* les 2 trains ne peuvent pas avoir l'autorisation de traverser en même temps la zone commune *)
AUT12.AUT34=0; 

RR13 : (* il faut que le train 12 soit devant un feu 12 ou dans la zone commune pour qu'il ait l'autorisation de traverser *)   
AUT12 <= (XR12+XR21+ZC12);        

RR14 : (* il faut que le train 34 soit devant un feu 34 ou dans la zone commune pour qu'il ait l'autorisation de traverser *)
AUT34 <= (XR34+XR43+ZC34);    

RR15 : (* pour que les 2 feux 12 soient verts, il faut avoir l'autorisation de traverser pour le train 12 et que l'aiguillage (monostable) soit bien positionné *)
FV12 <= TT_Limit12.AUT12;   

RR16 : (* pour que les 2 feux 34 soient verts, il faut avoir l'autorisation de traverser pour le train 34 et que l'aiguillage (monostable) soit bien positionné *)
FV34 <= TT_Limit34.AUT34; 


RR17 : (* Les feux 12 restent verts pendant que le train 12 traverse *)
ZC12 <= FV12;    

RR18 : (* Les feux 34 restent verts pendant que le train 34 traverse *)
ZC34 <= FV34;     
     
RR19 : (* si le train 12 est autorisé à traverser, l'aiguillage (monostable) doit être activé *)
AUT12 <= T_Turn;                          
                   
RR20 : (* si le train 34 est autorisé à traverser, l'aiguillage (monostable) doit être désactivé *)
AUT34 <= /T_Turn;       
       
          
</REQUIREMENTS>
<ASSUMPTIONS>
# Name : BooleanFormula = BooleanFormula (* Optional comment *) ;

A0 : (**)
ZC12.ZC34 = 0;

A1 : (**)
ZC12./TT_Limit12+ZC34./TT_Limit34 = 0;
 
</ASSUMPTIONS>                                                                    
<PRIORITIES>
# [Name|{Name, Name}] >> Name (* Optional comment *) ;
</PRIORITIES>
<OPTIMUM CRITERIA>
# Name : [Minimal|Maximal] (* Comment *)
#         BooleanFormula ;



</OPTIMUM CRITERIA>
</PROBLEM>

