<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 ;

M20 : Maximal (**)
AUT12;   

M21 : Maximal (**)
FV12;   

M22 : Maximal (**)
AUT34; 

M23 : Maximal (**)
FV34;   


M24 : Minimal (**)
T_Turn;  

</OPTIMUM CRITERIA>
</PROBLEM>


Global Boolean equations system building:
- Size of the BDD which represents the global assumption: 7
* SubProblem 1:
  - Number of unknowns: 7
  - Number of optimum criteria: 5
  - Size of the BDD which represents the Boolean equation: 72
  - Time spent: 4 ms
- Time spent for all systems building: 8 ms
Results:
* SubProblem 1:
  - Solutions:
[One]        T_Turn = ZC12+/ZC34.XR12+/ZC34.XR21
[One]          FV12 = ZC12+/ZC34.TT_Limit12.XR12+/ZC34.TT_Limit12.XR21
[One]          FV34 = ZC34+/ZC12.TT_Limit34./XR12.XR34./XR21+/ZC12.TT_Limit34./XR12.XR43./XR21
[One]          FR12 = ZC34+/TT_Limit12+/ZC12./XR12./XR21
[One]          FR34 = ZC12+/TT_Limit34+/ZC34.XR12+/ZC34.XR21+/ZC34./XR34./XR43
[One]         AUT12 = ZC12+/ZC34.XR12+/ZC34.XR21
[One]         AUT34 = ZC34+/ZC12./XR12.XR34./XR21+/ZC12./XR12.XR43./XR21
  - Optimum criteria:
[Max]              M20 = ZC12+/ZC34.XR12+/ZC34.XR21
[Max]              M21 = ZC12+/ZC34.TT_Limit12.XR12+/ZC34.TT_Limit12.XR21
[Max]              M22 = ZC34+/ZC12./XR12.XR34./XR21+/ZC12./XR12.XR43./XR21
[Max]              M23 = ZC34+/ZC12.TT_Limit34./XR12.XR34./XR21+/ZC12.TT_Limit34./XR12.XR43./XR21
[Min]              M24 = ZC12+/ZC34.XR12+/ZC34.XR21

Generation of the code :
T_Turn := ZC12 OR NOT ZC34 AND XR12 OR NOT ZC34 AND XR21;
FV12 := ZC12 OR NOT ZC34 AND TT_Limit12 AND XR12 OR NOT ZC34 AND TT_Limit12 AND XR21;
FV34 := ZC34 OR NOT ZC12 AND TT_Limit34 AND NOT XR12 AND XR34 AND NOT XR21 OR NOT ZC12 AND TT_Limit34 AND NOT XR12 AND XR43 AND NOT XR21;
FR12 := ZC34 OR NOT TT_Limit12 OR NOT ZC12 AND NOT XR12 AND NOT XR21;
FR34 := ZC12 OR NOT TT_Limit34 OR NOT ZC34 AND XR12 OR NOT ZC34 AND XR21 OR NOT ZC34 AND NOT XR34 AND NOT XR43;
AUT12 := ZC12 OR NOT ZC34 AND XR12 OR NOT ZC34 AND XR21;
AUT34 := ZC34 OR NOT ZC12 AND NOT XR12 AND XR34 AND NOT XR21 OR NOT ZC12 AND NOT XR12 AND XR43 AND NOT XR21;

Global Boolean equation solving:
* SubProblem 1:
  - The Boolean equations system has solutions. 
  - Time spent for resolution : 19 ms
- Time spent for all resolutions : 22 ms


Details of BDD operations:
- BDD nodes stored    : 1294
- Operations stored   : 1105
- Operations not made :  141
