with SystemPerfect, System do
  // propriétés universelles
  deadlock := any_s - src(any_t - self_epsilon);
  notResettable := any_s - coreach(initial, any_t);
  // Systèmes réactifs
  control := any_t & label action;
  uncontrol := any_t & label time;
  SR := any_s & ([T.level=0] | [T.level=4] | deadlock);
  LossCtrl := src(control) & SR;
  WinCtrl := src(control) - SR;
  LossEnv := src(uncontrol) - SR;
  WinEnv := src(uncontrol) & SR;
  /* Classical equations for
  *  - winning strategy (| for lfp and to reach winning states)
  *  - controller synthesis (& for gfp and to avoid loosing states)
  Winning           = Win |& src(WinningStep);
  WinningStep       = Step & rtgt(Loosing);
  Loosing           = Loss |& (src(LoosingStep) - src(NotLoosingStep));
  LoosingStep       = Step & rtgt(Winning);
  NonLoosingStep    = Step - rtgt(Winning);
  */
  WinningCtrl -=
    control & 
    rtgt(LossEnv & 
        (src(uncontrol & rtgt(WinCtrl & src(WinningCtrl))) - 
         src(uncontrol - rtgt(WinCtrl & src(WinningCtrl)))));
   project(any_s, (WinningCtrl|uncontrol,empty_t), 'Ctrl_$NODENAME', true,C) > 'Ctrl_$NODENAME.alt';
done