%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% PROBLEMS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
CHANGES NEEDED IN JCIRCUS:

- Implementation of pattern for axiomatic definition ok - \power
type ok - Check if single sync in an external choice will be
necessary - Generic and dotted channels

--AINDA SEM MODIFICAR!!!!-- (IR AO PRÓXIMO EXEMPLO)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% TYPES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{zed}
  AreaId ::= A0 | A1
\end{zed}

\begin{zed}
  ZoneId ::= Z0 | Z1 | Z2 | Z3 | Z4 | Z5
\end{zed}

\begin{zed}
  Mode ::= automatic | manual | disabled
\end{zed}

% Translator nao aceita abbreviations
% begin{zed}
%  SwitchMode == Mode \setminus \{ disabled \}
%\end{zed}

\begin{zed}
  OnOff ::= on | off
\end{zed}

\begin{zed}
  AlarmStage ::= alarmOff | firstStage | secondStage
\end{zed}

\begin{zed}
  LampId ::= zoneFaultLamp
                | earthFaultLamp
                | sounderLineFaultLamp
                | powerFaultLamp
                | isolateRemoteSignalLamp
                | actuatorLineFaultLamp
                | circuitFaultLamp
                | alarmSilencedLamp
                | systemOnLamp
\end{zed}

\begin{zed}
  FaultId ::= zoneFault
                | earthFault
                | sounderLineFault
                | powerFault
                | isolateRemoteSignal
                | actuatorLineFault
\end{zed}

\begin{zed}
  SystemState ::= fireSysStarts
                | fireSyss
                | fireSysDs
                | autos
                | countdowns
                | discharges
                | resets
                | manuals
                | disableds
\end{zed}

\begin{zed}
  Bool ::= ttrue | ffalse
\end{zed}

\begin{axdef}
    getZones: AreaId \pinj \power ZoneId
\where
    (getZones ~ A0) = \{~ Z0, Z1 ~\} \land
    (getZones ~ A1) = \{~ Z2, Z3 ~\}
\end{axdef}

\begin{axdef}
    getLampId: FaultId \pinj LampId
\where
    getLampId ~ zoneFault = zoneFaultLamp  \land
    getLampId ~ earthFault = earthFaultLamp  \land
    getLampId ~ sounderLineFault = sounderLineFaultLamp  \land
    getLampId ~ powerFault = powerFaultLamp  \land
    getLampId ~ isolateRemoteSignal = isolateRemoteSignalLamp  \land
    getLampId ~ actuatorLineFault = actuatorLineFaultLamp
\end{axdef}

\begin{axdef}
    gasDelay: \nat
\where
    gasDelay = 30
\end{axdef}

\begin{circus}
    \circchannel switchOn, silenceAlarm, startClock, clockFinished
\end{circus}

\begin{circus}
    \circchannel detection: ZoneId
\end{circus}

Obs: era SwitchMode
\begin{circus}
    \circchannel modeSwitch: Mode
\end{circus}

\begin{circus}
    \circchannel externalManualDischarge: \power AreaId
\end{circus}

\begin{circus}
    \circchannel fault: FaultId
\end{circus}

\begin{circus}
    \circchannel reset, actuatorsReplaced
\end{circus}

\begin{circus}
    \circchannel alarm: AlarmStage
\end{circus}

\begin{circus}
    \circchannel [T] switchLamp: T \cross OnOff
\end{circus}

\begin{circus}
    \circchannel switchBuzzer: OnOff
\end{circus}

\begin{circus}
    \circchannel systemState: SystemState
\end{circus}

%% Created in data refinement

\begin{circus}
    \circchannel displayDischarge, manualDischarge : \power AreaId
\end{circus}

\begin{circus}
    \circchannel switched, automaticDischarge, anyDischarge, noDischarge,
    countdown, counting \\%
\end{circus}

\begin{circus}
    \circchannel gasDischarged, gasNotDischarged: AreaId %
\end{circus}

\begin{circus}
    \circchannelset GasDischargeSync ==
        \lchanset
            manualDischarge, automaticDischarge, countdown, counting,
            gasDischarged, gasNotDischarged, anyDischarge, noDischarge
        \rchanset
\end{circus}

\begin{circus}
    \circchannelset\ Sigma2 ==
        \lchanset
            switchOn, reset, detection, modeSwitch, silenceAlarm,
            actuatorsReplaced,

            manualDischarge, automaticDischarge, countdown, counting,
            gasDischarged, gasNotDischarged, anyDischarge, noDischarge
        \rchanset
\end{circus}

\begin{circus}
    \circchannelset\ Sigmaareas == \lchanset
            switchOn, reset, modeSwitch, detection,
            silenceAlarm, actuatorsReplaced,
            automaticDischarge, manualDischarge,
            anyDischarge, noDischarge, counting \rchanset
\end{circus}

\begin{circus}
    \circchannelset\ DisplaySync == \lchanset displayDischarge, switched \rchanset
\end{circus}

\begin{circus}
    \circchannelset\ Sigma1 == \lchanset
        switchOn, reset, detection, displayDischarge,
        silenceAlarm, actuatorsReplaced, fault \rchanset
\end{circus}

%DAQUI PARA BAIXO PODE DAR ALGUMA COISA!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

\begin{circus}
    \circprocess FireControl \circdef \circbegin
\end{circus}

%\begin{circus}
%    \circstate
%end{circus}

%    \begin{schema}{InternalSystemState}
    \begin{circusaction}
        \circstate
        InternalSystemState ~~==~~ [~mode1: Mode~]
    \end{circusaction}

    \begin{circusaction}
        InitFireControl \circdef mode1 := automatic
    \end{circusaction}

    \begin{circusaction}
        SwitchFireControlMode \circdef newMode: Mode \circspot mode1 := newMode
    \end{circusaction}

    \begin{circusaction}
        SwitchFireControl2AutomaticMode \circdef mode1 := automatic
    \end{circusaction}

    \begin{circusaction}
        SwitchFireControl2DisabledMode \circdef mode1 := disabled
    \end{circusaction}

    \begin{circusaction}
    FireSysStart \circdef
        systemState!fireSysStarts \then switchOn \then
            switched \then InitFireControl \circseq FireSys
    \end{circusaction}

    \begin{circusaction}
    FireSys \circdef
        systemState!fireSyss \then
            (
            modeSwitch?newMode \then (SwitchFireControlMode(newMode) \circseq
            FireSys)
            \extchoice
            (detection?newZone \then switched \then alarm!firstStage \then
                \circif (mode1 = manual) \circthen Manual 
                \circelse (mode1 = automatic) \circthen Auto
                \circfi
            )
            \extchoice
            actuatorsReplaced \then switched \then
            (SwitchFireControl2AutomaticMode \circseq Reset)
            \extchoice
            (fault?faultId \then switched \then FireSys)
            )
    \end{circusaction}

    \begin{circusaction}
    Manual \circdef
        systemState!manuals \then
            ((detection?newZone \then switched \then Manual)
            \extchoice
            (silenceAlarm \then switched \then alarm!alarmOff \then Reset)
            \extchoice
            externalManualDischarge?areas \then (manualDischarge!areas \then
                \circvar log: \power AreaId \circspot (
                    (log := \emptyset) \circseq
                    (\Semi area: AreaId \circspot (
                        (gasDischarged.area \then log := (log \cup \{ area \}))
                        \extchoice
                        (gasNotDischarged.area \then \Skip)
                        )
                    ) \circseq
                    ( \lcircguard log \neq \emptyset \rcircguard \circguard
                        anyDischarge \then (displayDischarge!log \then switched
                        \then SwitchFireControl2DisabledMode \circseq Reset)
                    \extchoice
                    ( \lcircguard 
                    	log = \emptyset \rcircguard \circguard
                        noDischarge \then Manual)
                    )
                )
            )
            \extchoice
            (fault?faultId \then switched \then Manual)
            )
    \end{circusaction}

    \begin{circusaction}
    Auto \circdef
        systemState!autos \then
            ((reset \then (switched \then InitFireControl \circseq FireSys))
            \extchoice
            (detection?newZone \then switched \then Auto)
            \extchoice
            (countdown \then counting \then alarm!secondStage \then Countdown)
            \extchoice
            (fault?faultId \then switched \then Auto)
            )
    \end{circusaction}

    \begin{circusaction}
    Reset \circdef
        systemState!resets \then
            ((detection?newZone \then switched \then Reset)
            \extchoice
            (reset \then switched \then
                \circif (mode1 = disabled) \circthen FireSysD
                \circelse (mode1 \neq disabled) \circthen (InitFireControl
                \circseq FireSys)
                \circfi
            )
            \extchoice
            (actuatorsReplaced \then switched \then
            (SwitchFireControl2AutomaticMode \circseq Reset))
            \extchoice
            (fault?faultId \then switched \then Reset)
            )
    \end{circusaction}

    \begin{circusaction}
    WaitingClock \circdef
        (detection?newZone \then switched \then WaitingClock)
        \extchoice
        (clockFinished \then Discharge)
        \extchoice
        (fault?faultId \then switched \then Reset)
    \end{circusaction}

    \begin{circusaction}
    Countdown \circdef systemState!countdowns \then startClock \then WaitingClock
    \end{circusaction}

    \begin{circusaction}
    FireSysD \circdef
        systemState!fireSysDs \then
            ((detection?newZone \then switched \then alarm!firstStage \then Disabled)
            \extchoice
            (actuatorsReplaced \then (switched \then InitFireControl \circseq
            FireSys))
            \extchoice
            (fault?faultId \then switched \then FireSysD)
            )
    \end{circusaction}

    \begin{circusaction}
    Discharge \circdef
        systemState!discharges \then automaticDischarge \then
            \circvar\ log: \power AreaId \circspot (
                (log := \emptyset) \circseq
                (\Semi area: AreaId \circspot (
                    (gasDischarged.area \then log := (log \cup \{ area \}))
                    \extchoice
                    (gasNotDischarged.area \then \Skip)
                )
                ) \circseq
                anyDischarge \then displayDischarge!log \then switched \then
                    SwitchFireControl2DisabledMode \circseq Reset
            )
    \end{circusaction}

    \begin{circusaction}
    Disabled \circdef
        systemState!disableds \then
            ((detection?newZone \then switched \then Disabled)
            \extchoice
            (silenceAlarm \then switched \then alarm!alarmOff \then Reset)
            \extchoice
            (fault?faultId \then switched \then Disabled)
            )
    \end{circusaction}

\begin{circusaction}
    \circspot FireSysStart
\end{circusaction}

\begin{circus}
    \circend
\end{circus}

%DAQUI PARA BAIXO TAMBÉÉÉÉÉM PODE DAR ALGUMA COISA

\begin{circus}
\circprocess\ Area \circdef\ ident: AreaId \circspot \circbegin
\end{circus}

    \begin{circusaction}
        \circstate AreaState ~~==~ [~ mode: Mode ; controlledZones: \power
        ZoneId ; activeZones: \power ZoneId ; discharge: Bool ; active: Bool \where controlledZones = getZones~ident \land (mode=automatic) \implies active=ttrue \iff \# activeZones \geq 2 \land (mode=manual) \implies active=ttrue \iff \# activeZones \geq 1 \land activeZones \subseteq controlledZones ~]
	\end{circusaction}

    \begin{circusaction}
    InitArea \circdef 
    	activeZones := \emptyset \circseq 
    	discharge := ffalse
    \circseq mode := automatic
    \end{circusaction}

    \begin{circusaction}
    SwitchAreaMode \circdef newMode: Mode \circspot mode := newMode
    \end{circusaction}

    \begin{circusaction}
    SwitchArea2AutomaticMode \circdef mode := automatic
    \end{circusaction}

    \begin{circusaction}
    SwitchArea2DisabledMode \circdef mode := disabled
    \end{circusaction}

    \begin{circusaction}
    ActivateZone \circdef newZone: ZoneId \circspot (
        \circif newZone \in
        controlledZones
        \circthen activeZones := (activeZones \cup \{newZone\})
        \circfi
    )
    \end{circusaction}

    \begin{circusaction}
    AutomaticDischarge \circdef discharge := active
    \end{circusaction}

    \begin{circusaction}
    ManualDischarge \circdef pAreas: \power AreaId \circspot (
        \circif ident \in pAreas \land active = ttrue \circthen discharge :=
        ttrue \circelse \lnot(ident \in pAreas \land active = ttrue) \circthen
        discharge := ffalse
        \circfi
    )
    \end{circusaction}

    \begin{circusaction}
    StartArea \circdef switchOn \then InitArea \circseq AreaCycle
    \end{circusaction}

    \begin{circusaction}
    AreaCycle \circdef
        (actuatorsReplaced \then (SwitchArea2AutomaticMode \circseq ResetArea))
        \extchoice 
        (modeSwitch?newMode \then (SwitchAreaMode(newMode) \circseq AreaCycle))
        \extchoice 
        (detection?newZone \then (ActivateZone(newZone) \circseq
            \circif (mode = automatic) \circthen AutoArea
            \circelse (mode = manual) \circthen ManualArea
            \circfi)
        )   
    \end{circusaction}

    \begin{circusaction}
    AutoArea \circdef
        \circif (active = ttrue) \circthen 
            countdown \then counting \then WaitingDischarge
        \circelse (active = ffalse) \circthen
                ((reset \then (InitArea \circseq AreaCycle))
                \extchoice 
                (detection?newZone \then (ActivateZone(newZone) \circseq AutoArea))
                \extchoice 
                (counting \then WaitingDischarge)
                )
        \circfi
    \end{circusaction}

    \begin{circusaction}
    ManualArea \circdef
        (silenceAlarm \then ResetArea)
        \extchoice 
        (detection?newZone \then (ActivateZone(newZone) \circseq ManualArea))
        \extchoice 
        (manualDischarge?areas \then 
            (ManualDischarge(areas) \circseq
                \circif (discharge = ttrue) \circthen gasDischarged.ident \then
                \Skip \circelse (discharge = ffalse) \circthen
                gasNotDischarged.ident \then \Skip
                \circfi
                \circseq
                ((anyDischarge \then (SwitchArea2DisabledMode \circseq ResetArea))
                \extchoice 
                (noDischarge \then ManualArea)
                )
            )
        )
    \end{circusaction}

    \begin{circusaction}
    WaitingDischarge \circdef
        (detection?newZone \then WaitingDischarge)
        \extchoice 
        (automaticDischarge \then 
            (AutomaticDischarge \circseq
                \circif (discharge = ttrue) \circthen gasDischarged.ident \then
                \Skip \circelse (discharge = ffalse) \circthen
                gasNotDischarged.ident \then \Skip
                \circfi
                \circseq
                anyDischarge \then SwitchArea2DisabledMode \circseq ResetArea
            )
        )
    \end{circusaction}

    \begin{circusaction}
    ResetArea \circdef
        (detection?newZone \then (ActivateZone(newZone) \circseq ResetArea))
        \extchoice 
        (reset \then
            (\circif (mode = disabled) \circthen AreaD
            \circelse (mode \neq disabled) \circthen InitArea \circseq AreaCycle
            \circfi)
        )    
        \extchoice 
        (actuatorsReplaced \then (SwitchArea2AutomaticMode \circseq ResetArea))
    \end{circusaction}

    \begin{circusaction}
    AreaD \circdef
        (detection?newZone \then (ActivateZone(newZone) \circseq DisabledArea))
        \extchoice 
        (actuatorsReplaced \then (InitArea \circseq AreaCycle))
    \end{circusaction}

    \begin{circusaction}
    DisabledArea \circdef
       (detection?newZone \then (ActivateZone(newZone) \circseq DisabledArea))
       \extchoice 
       (silenceAlarm \then ResetArea)
    \end{circusaction}

\begin{circusaction}
    \circspot StartArea
\end{circusaction}

\begin{circus}
    \circend
\end{circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% CONCRETE AREAS PROCESS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
    \circprocess\ ConcreteAreas \circdef\ \Parallel ident: AreaId %\circspot
    \lpar Sigmaareas \rpar \circspot
    Area(ident)
\end{circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% DISPLAY CONTROLLER PROCESS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
    \circprocess\ DisplayController \circdef \circbegin
\end{circus}

    \begin{circusaction}
    StartDisplay \circdef
        switchOn \then switchLamp[LampId].systemOnLamp!on \then
            switched \then DisplayCycle
    \end{circusaction}

    %:: begin{circus}
%    SwitchLampsOff \circdef
%        ((switchBuzzer!off \then \\Skip)
%            \linter \rinter
%        (\Interleave id: (LampId \setminus \{circuitFaultLamp,systemOnLamp\})
%        \circspot switchLamp[LampId].id!off \then \\Skip)) \linter \rinter
%        ((\Interleave zone:ZoneId \circspot switchLamp[ZoneId].zone!off \then
%        \\Skip) \linter \rinter
%        (\Interleave area:AreaId \circspot switchLamp[AreaId].area!off \then
%       \\Skip)) :: end{circus}
  As the strategy does not accept iterated interleaving, I have to expand this
  for all the types.
  AreaId ::= A0 | A1
  ZoneId ::= Z0 | Z1 | Z2 | Z3 | Z4 | Z5
  LampId ::= zoneFaultLamp
                | earthFaultLamp
                | sounderLineFaultLamp
                | powerFaultLamp
                | isolateRemoteSignalLamp
                | actuatorLineFaultLamp
                | circuitFaultLamp
                | alarmSilencedLamp
                | systemOnLamp
\{circuitFaultLamp,systemOnLamp\}

    \begin{circusaction}
    SwitchLampsOff \circdef
    (   ( ((switchBuzzer!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[LampId].zoneFaultLamp!off \then \Skip))
            \linter \{ \} | \{ \} \rinter
        ((switchLamp[LampId].earthFaultLamp!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[LampId].sounderLineFaultLamp!off \then \Skip)) )
            \linter \{ \} | \{ \} \rinter
       ( ((switchLamp[LampId].isolateRemoteSignalLamp!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[LampId].actuatorLineFaultLamp!off \then \Skip))
            \linter \{ \} | \{ \} \rinter
        ((switchLamp[LampId].alarmSilencedLamp!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[ZoneId].Z0!off \then \Skip)) )   )
            \linter \{ \} | \{ \} \rinter
    (   ( ((switchLamp[ZoneId].Z1!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[ZoneId].Z2!off \then \Skip))
            \linter \{ \} | \{ \} \rinter
        ((switchLamp[ZoneId].Z3!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[ZoneId].Z4!off \then \Skip)) )
            \linter \{ \} | \{ \} \rinter
       ( ((switchLamp[ZoneId].Z5!off \then \Skip)
            \linter \{ \} | \{ \} \rinter
        (switchLamp[AreaId].A0!off \then \Skip))
            \linter \{ \} | \{ \} \rinter
        (switchLamp[AreaId].A1!off \then \Skip) )   )
    \end{circusaction}

    \begin{circusaction}
    DisplayCycle \circdef
        (detection?zone \then switchLamp[~ZoneId~].zone!on \then switched \then
        DisplayCycle)
        \extchoice 
        (fault?faultId \then switchLamp[~LampId~].(getLampId~faultId)!on \then
            switchBuzzer!on \then switched \then DisplayCycle)
        \extchoice 
        (silenceAlarm \then switchLamp[~LampId~].alarmSilencedLamp!on \then
            switched \then DisplayCycle)
        \extchoice 
        (displayDischarge?areas \then
            ((\Semi area: areas \circspot
                switchLamp[~AreaId~].area!on \then \Skip
            ) \circseq
            switchLamp[~LampId~].circuitFaultLamp!on \then switched \then
            DisplayCycle ))
        \extchoice 
        (reset \then (SwitchLampsOff \circseq switched \then DisplayCycle))
        \extchoice 
        (actuatorsReplaced \then switchLamp[LampId].circuitFaultLamp!off \then switched \then DisplayCycle)
    \end{circusaction}

\begin{circusaction}
    \circspot StartDisplay
\end{circusaction}

\begin{circus}
    \circend
\end{circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% CONCRETE INTERNAL SYSTEM PROCESS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
    \circprocess\ ConcreteInternalSystem \circdef
        (FireControl \lpar Sigma1 \rpar DisplayController) \circhide
        DisplaySync
\end{circus}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% CONCRETE FIRE CONTROL PROCESS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{circus}
    \circprocess ConcreteFireControl \circdef
        (
        ConcreteInternalSystem 
        \lpar Sigma2 \rpar 
        ConcreteAreas
        ) 
        \circhide
        GasDischargeSync
\end{circus}
