plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/examples/fe/triple_modular_generator/SC_TMG_CC.fei

/-- Description of the whole fault extension
    (multiline)
--/
FAULT EXTENSION FE_SC_TMG

  EXTENSION OF MODULE Generator
     /-- Description of Fault Slice Gen_StuckOff --/
     SLICE Gen_StuckOff AFFECTS state WITH

       /-- Description of fault mode stuckAt_Off --/
       MODE stuckAt_Off : Permanent StuckAtByValue_D(
    		  data term << off,
                  data input << state,
                  data varout >> state,
                  event failure >> fault_event_stuck_at_off);


  EXTENSION OF MODULE Switch

     /-- Description of Fault Model for Switch --/
     SLICE Switch_StuckClosed_StuckOpen
      AFFECTS state WITH

        /-- Description of fault mode StuckAt_Closed --/
        MODE stuckAt_Closed : Transient StuckAtByValue_D(
                  data term << closed,
                  data input << state,
                  data varout >> state,
                  template self_fix = self_fixed,
                  event failure >> fault_event_stuck_at_closed,
                  event self_fixed >> nominal_event);

        /-- Description of fault mode StuckAt_Open --/
        MODE stuckAt_Open : Transient StuckAtByValue_D(data term << open,
                  data input << state,
                  data varout >> state,
                  template self_fix = self_fixed,
                  event failure >> fault_event_stuck_at_open,
                  event self_fixed >> nominal_event);

  COMMON CAUSES
       CAUSE CC2
         MODULE Generator
           FOR INSTANCES SC.G[12]
           MODE Gen_StuckOff.stuckAt_Off WITHIN 0 .. 0;

       CAUSE CC3
         MODULE Generator
           MODE Gen_StuckOff.stuckAt_Off WITHIN 1 .. 2;