(* Version with  do_for_all
   2 Agents and with Inter-Node-Communication,
   i.e. Home(l)=agent(1) also requests on l! 
   MessInTrQ with parametric length 
   clear InMess, as far as appending to MessInTr is successful
*)
(*-----------------------------------------------------*)

freetype  TYPE    == { noMess, get, getx, inv,  wb, rpl, fwdack, swb, 
                      invack,  nack, nackc, fwdget, fwdgetx, put, putx,
                      nackc2, put_swb, putx_fwdack          (*for intra-node-comm*)
                      }

freetype  CCTYPE  == { ccget, ccgetx, ccrpl, ccwb }

freetype  AGENT   == { agent :INT, none }
freetype  LINE    == { lines :INT }
typealias MESSAGE == AGENT * TYPE * AGENT * LINE

freetype PHASE  == { ready, wait, invalidPhase }
freetype STATE   == { exclusive, shared, invalid }
freetype LENGTH == { n :INT }
(*------------------------------------------*)
static function max_agent == 2
static function max_line  == 2
static function maxQ  == 2

static function Agent == {agent(i)| i in {1..max_agent}} union {none}
static function Agent_without_none == {agent(i)| i in {1..max_agent}}
static function Line  == { lines(i) | i in {1..max_line} }
static function QLength  == { n(i) | i in {1..maxQ} }
(*------------------------------------------*)
static function Type  == { noMess, get, getx, inv,  wb, rpl, fwdack, swb, 
                           invack,  nack, nackc, fwdget, fwdgetx, put, putx,
                           nackc2, put_swb, putx_fwdack                      (*for intra-node-comm*)
                           }

static function CCType == { ccget, ccgetx, ccrpl, ccwb }
static function ReqType == { noMess, get, getx, rpl, wb }


static function Home ==
  MAP_TO_FUN { lines(1) -> agent(1), lines(4) -> agent(1),
               lines(2) -> agent(1), lines(5) -> agent(2),
               lines(3) -> agent(3), lines(6) -> agent(3) }

(*------------------------------------------*)
(* --- NEW: Messages in Transit ------------*)

(*-- NEW: in order to make undef uneccassary initialize -- *)

dynamic function MessInTr : LENGTH * AGENT -> TYPE
  with MessInTr(i,a) in Type
  initially MAP_TO_FUN {(i,a) -> noMess|(i,a) in Union({ {(i,a) | i in QLength } | a in Agent\{none}}) }

dynamic function SenderInTr : LENGTH * AGENT -> AGENT
   with SenderInTr(i,a) in Agent \ { none }
   initially MAP_TO_FUN { (i,a) -> agent(1) | (i,a) in Union 
                           ({ { (i,a) | i in QLength } | a in Agent \ { none }}) }

dynamic function SourceInTr : LENGTH * AGENT -> AGENT
   with SourceInTr(i,a) in Agent \ { none }
  initially MAP_TO_FUN { (i,a) -> agent(1) | (i,a) in Union 
                           ({ { (i,a) | i in QLength } | a in Agent \ { none }}) }


dynamic function LineInTr : LENGTH * AGENT -> LINE
  with LineInTr(i,a) in Line
  initially MAP_TO_FUN { (i,a) -> lines(1) | (i,a) in Union 
                           ({ { (i,a) | i in QLength } | a in Agent \ { none }}) }

(*------------------------------------------*)
(*-- NEW: in order to make undef uneccassary -- *)
dynamic function SenderInTrR : AGENT -> AGENT
   with SenderInTrR(a) in Agent \ { none }
  initially MAP_TO_FUN { a -> agent(2) | a in Agent \ { none } }

(*-- NEW: in order to make undef uneccassary -- *)
dynamic function SourceInTrR : AGENT -> AGENT
   with SourceInTrR(a) in Agent \ { none }
  initially MAP_TO_FUN { a -> agent(1) | a in Agent \ { none } }

(*-- NEW: in order to make undef uneccassary -- *)
dynamic function MessInTrR : AGENT -> TYPE
  with MessInTrR(a) in ReqType
  initially MAP_TO_FUN { a -> noMess | a in Agent \ { none } }

(*-- NEW: initial value changed from undef to line(1) --*)
dynamic function LineInTrR : AGENT -> LINE
  with LineInTrR(a) in Line
  initially MAP_TO_FUN { a -> lines(1) | a in Agent \ { none } }


(*------------------------------------------*)
(* --- New: Mess after Transit -------------*)


(*-- NEW: in order to make undef uneccassary -- *)
dynamic function InSender : AGENT -> AGENT
   with InSender(a) in Agent \ { none }
  initially MAP_TO_FUN { a -> agent(2) | a in Agent \ { none } }

(*-- NEW: in order to make undef uneccassary -- *)
dynamic function InSource : AGENT -> AGENT
   with InSource(a) in Agent \ { none }
  initially MAP_TO_FUN { a -> agent(2) | a in Agent \ { none } }

(*-- NEW: in order to make undef uneccassary -- *)
dynamic function InMess : AGENT -> TYPE
  with InMess(a) in Type
  initially MAP_TO_FUN { a -> noMess | a in Agent \ { none } }

(*-- NEW: initial value changed from undef to line(1) --*)
dynamic function InLine : AGENT -> LINE
  with InLine(a) in Line
  initially MAP_TO_FUN { a -> lines(1) | a in Agent \ { none } }

  
(*------------------------------------------*)
(*---- other state and line Variables ----*)

dynamic function CurPhase :AGENT * LINE -> PHASE
   initially MAP_TO_FUN
    { (a,l) -> ready | (a,l) in Union ({ { (a,l) | 
                     a in Agent \ { none }} | l in Line} )}

(*-- NEW: initial value changed from shared to invalid --*)
dynamic function CCState :AGENT * LINE -> STATE
   initially MAP_TO_FUN 
    { (a,l) -> invalid | (a,l) in Union ({ { (a,l) | a in 
                                      Agent \ { none }} | l in Line} )}

dynamic relation Pending  :LINE
   initially SET_TO_REL {}

dynamic function Owner    :LINE -> AGENT
   with Owner (l) in Agent
   initially MAP_TO_FUN { l -> none | l in Line }

dynamic relation Sharer   :LINE * AGENT
   initially SET_TO_REL {}


(*------------------------------------------*)
(*-- synchronization -----------------------*)

freetype MODE   == { behave, sync }

dynamic function toggle : MODE
   initially behave

(*------------------------------------------*)

external function Self    :AGENT
  with Self in Agent \ { none }

external function produce :AGENT -> (CCTYPE * LINE)
    with produce(a) in Union ({ { (cctype_, line_) | cctype_ in CCType } | line_ in Line }) 
(*   initially MAP_TO_FUN { a -> (ccget,lines(1)) | a in Agent \ { none } } *)




(*-------------------------------------------------------------*)


transition AppendToTransit (agent_, (sender_,mess_,source_,line_)) ==
   if MessInTr(n(1),agent_)=noMess
   then  SenderInTr(n(1),agent_) := sender_ 
         MessInTr(n(1),agent_)  := mess_ 
         SourceInTr(n(1),agent_):= source_ 
         LineInTr(n(1),agent_)  := line_
   else do forall i in { 2..maxQ }                           (* the first empty Queue-entry *)
         if MessInTr(n(i-1),agent_)!=noMess and MessInTr(n(i),agent_)=noMess 
         then SenderInTr(n(i),agent_) := sender_ 
              MessInTr(n(i),agent_)  := mess_ 
              SourceInTr(n(i),agent_):= source_ 
              LineInTr(n(i),agent_)  := line_
         endif
        enddo
   endif


transition AppendRequestToTransit (agent_, (sender_,mess_,source_,line_)) ==
  if MessInTrR (agent_)=noMess
  then SenderInTrR(agent_) := sender_ 
       MessInTrR (agent_)  := mess_ 
       SourceInTrR (agent_):= source_ 
       LineInTrR (agent_)  := line_
  endif


(*-------------------------------------------------------------*)
(*-- not excluding intra-node-comm add:  and Self != Home(l)   *)
(*-- restricting requests: if line is shared or owned dont 
     make a new request!                                     --*)
(* The guard for sending a request have to be satisfied when
   the request is passing through also!! Not only when the request is put into 
   Transit-Queue! *)


transition R1_R2_R3_R4 ==
  if MessInTrR(agent(1)) = noMess 
  then 
    case produce(Self) of
      (ccget, l) :
         if CurPhase(Self, l)=ready
         then AppendRequestToTransit (Home(l),(Self,get,Self,l))
         endif;
      (ccgetx,l) :
         if CurPhase(Self, l)=ready
         then AppendRequestToTransit (Home(l), (Self,getx,Self,l))
         endif;
      (ccrpl,l) :
          if CurPhase(Self, l)=ready and CCState(Self,l)=shared
          then AppendRequestToTransit (Home(l),(Self,rpl,Self,l))
          endif;
       (ccwb,l) :
          if CurPhase(Self, l)=ready and CCState(Self,l)=exclusive
          then AppendRequestToTransit (Home(l),(Self,wb,Self,l))
          endif;
     _ : skip
    endcase
  endif 


(*------------------------------------------------------------ *)


(*--------------------------------------------------------*)

transition R5 ==
  if (InMess(Self)=get and Home(InLine(Self)) = Self)
  then
     if Pending (InLine(Self))
      then if  MessInTr(n(maxQ),InSource(Self))=noMess
           then AppendToTransit (InSource(Self),
                         (Self,nack,InSource(Self),InLine(Self)))
                InMess(Self):=noMess
           endif
      else if Owner (InLine(Self)) != none
	     then if MessInTr(n(maxQ),Owner(InLine(Self)))=noMess
		  then AppendToTransit (Owner (InLine(Self)),
                          (Self,fwdget,InSource(Self),InLine(Self)))
		       Pending (InLine(Self)) := true
                       InMess(Self):=noMess
		  endif
           else if MessInTr(n(maxQ),InSource(Self))=noMess
		  then AppendToTransit (InSource(Self),
                          (Self,put,InSource(Self),InLine(Self)))
                       InMess(Self):=noMess
		       Sharer (InLine(Self), InSource(Self)) := true
		  endif
           endif
      endif
  endif


transition R6 ==
  if InMess(Self) = fwdget 
  then if CCState (Self,InLine(Self)) = exclusive
       then if (Home(InLine(Self))=InSource(Self))
            then if MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                 then AppendToTransit ( Home(InLine(Self)), (Self,put_swb,InSource(Self),InLine(Self)))
                      CCState(Self,InLine(Self)):=shared
                      InMess(Self):=noMess
                 endif
            else if MessInTr(n(maxQ),InSource(Self)) = noMess and MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                 then AppendToTransit (InSource(Self), (Self,put,InSource(Self),InLine(Self)))
                      AppendToTransit ( Home(InLine(Self)), (Self,swb,InSource(Self),InLine(Self)))
                      CCState(Self,InLine(Self)):=shared
                      InMess(Self):=noMess
                 endif
            endif
       else if (Home(InLine(Self))=InSource(Self))
            then if MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                 then AppendToTransit (Home(InLine(Self)),(Self,nackc2,InSource(Self),InLine(Self)))
                      InMess(Self):=noMess
                 endif
            else if MessInTr(n(maxQ),InSource(Self)) = noMess and MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                 then AppendToTransit (InSource(Self), (Self,nack,InSource(Self),InLine(Self)))
                      AppendToTransit (Home(InLine(Self)), (Self,nackc,InSource(Self),InLine(Self)))
                      InMess(Self):=noMess
                 endif
            endif
      endif
  endif

transition R7 ==
 if InMess(Self) = put
 then if CurPhase(Self,InLine(Self)) != invalidPhase
      then CCState(Self,InLine(Self)) := shared
      endif
      CurPhase(Self,InLine(Self)) := ready
      InMess(Self) := noMess
  endif

transition R8 ==
  if (InMess(Self) = swb and Home(InLine(Self)) = Self)
  then  
      Sharer(InLine(Self), InSource(Self)) := true
      if Owner(InLine(Self)) != none
      then Sharer(InLine(Self), Owner(InLine(Self))) := true
      endif
      Owner(InLine(Self)) := none
      Pending(InLine(Self)) := false
      InMess(Self) := noMess
  endif

(*-------------------------------------------------------------*)
(* if intra-node-comm and Home ask for getting then do put and swb in one step  *)

transition R7_R8 ==
 if InMess(Self) = put_swb
 then if CurPhase(Self,InLine(Self)) != invalidPhase
        then CCState(Self,InLine(Self)) := shared
      endif
      CurPhase(Self,InLine(Self)) := ready
      Sharer(InLine(Self), InSource(Self)) := true
      if Owner(InLine(Self)) != none
        then Sharer(InLine(Self), Owner(InLine(Self))) := true
      endif
      Owner(InLine(Self)) := none
      Pending(InLine(Self)) := false
      InMess(Self) := noMess
  endif
 


(*-------------------------------------------------------------*)

transition R9 ==
  if InMess(Self) = nack
  then
      CurPhase(Self, InLine(Self)) := ready
      InMess(Self) := noMess
  endif

transition R10 ==
 if (InMess(Self) = nackc and Home(InLine(Self)) = Self)
 then 
      Pending(InLine(Self)) := false
      InMess(Self) := noMess
  endif

(*-------------------------------------------------------------*)
(* if intra-node-comm and Home gets negativ request then do nack and nackc in one step  *)

transition R9_R10 ==
  if InMess(Self) = nackc2
  then
      CurPhase(Self, InLine(Self)) := ready
      Pending(InLine(Self)) := false
      InMess(Self) := noMess
  endif


(*-------------------------------------------------------------*)

transition R11 == 
  if (InMess(Self) = getx and Home(InLine(Self)) = Self)
  then
      if Pending(InLine(Self)) = true
      then if MessInTr(n(maxQ),InSource(Self)) = noMess
           then AppendToTransit (InSource(Self), (Self,nack,InSource(Self),InLine(Self)))
                InMess(Self):=noMess
           endif
      else if Owner(InLine(Self)) != none
           then if MessInTr(n(maxQ),Owner(InLine(Self))) = noMess
                then AppendToTransit (Owner(InLine(Self)),(Self,fwdgetx,InSource(Self),InLine(Self)))
                     Pending(InLine(Self)) := true
                     InMess(Self):=noMess
                endif
           else if ( forall agent_ in Agent_without_none : not(Sharer(InLine(Self),agent_)) )
                  then if MessInTr(n(maxQ),InSource(Self)) = noMess
                       then AppendToTransit (InSource(Self), (Self,putx,InSource(Self),InLine(Self)))
                          Owner(InLine(Self)) := InSource(Self)
                          InMess(Self):=noMess
                     endif
                else if (forall agent_ in Agent_without_none 
                                : not(Sharer(InLine(Self),agent_)) or MessInTr(n(maxQ),agent_) = noMess )
                     then do forall agent_ in Agent_without_none with Sharer(InLine(Self),agent_)
                                 AppendToTransit (agent_,(Self,inv,InSource(Self),InLine(Self)))
                                 Pending(InLine(Self)):=true
                          enddo
                          InMess(Self):=noMess
                     endif
                endif
           endif
      endif
  endif


(*--------------------------------------------------------------*)

transition R12 == 
  if InMess(Self) = fwdgetx
  then
      if CCState(Self,InLine(Self)) = exclusive
      then if (Home(InLine(Self))=InSource(Self))
           then if MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                then AppendToTransit (Home(InLine(Self)),(Self,putx_fwdack,InSource(Self),InLine(Self)))
                     CCState(Self,InLine(Self)):=invalid
                     InMess(Self):=noMess
                endif
           else if MessInTr(n(maxQ),InSource(Self)) = noMess and MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                then AppendToTransit (InSource(Self), (Self,putx,InSource(Self),InLine(Self)))
                     AppendToTransit (Home(InLine(Self)), (Self,fwdack,InSource(Self),InLine(Self)))
                     CCState(Self,InLine(Self)):=invalid
                     InMess(Self):=noMess
                endif
           endif
      else if (Home(InLine(Self))=InSource(Self))
           then if MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                then AppendToTransit (InSource(Self), (Self,nackc2,InSource(Self),InLine(Self)))
                     InMess(Self):=noMess
                endif
           else if MessInTr(n(maxQ),InSource(Self)) = noMess and MessInTr(n(maxQ),Home(InLine(Self))) = noMess
                then AppendToTransit (InSource(Self), (Self,nack,InSource(Self),InLine(Self)))
                     AppendToTransit (Home(InLine(Self)), (Self,nackc,InSource(Self),InLine(Self)))
                     InMess(Self):=noMess
                endif
           endif
      endif
  endif



transition R13 == 
  if InMess(Self) = putx
  then
      CCState(Self,InLine(Self)) := exclusive
      CurPhase(Self, InLine(Self)) := ready
      InMess(Self) := noMess
  endif

transition R14 == 
  if (InMess(Self) = fwdack and Home(InLine(Self)) = Self)
  then
      Owner(InLine(Self)) := InSource(Self)
      Pending(InLine(Self)) := false
      InMess(Self) := noMess
  endif

(*----------------------------------------------------------------------*)
(* if intra-node-comm and Home requests for exclusive mem then do putx and fwdack in one step  *)

transition R13_R14 == 
  if InMess(Self) = putx_fwdack
  then
      CCState(Self,InLine(Self)) := exclusive
      CurPhase(Self, InLine(Self)) := ready
      Owner(InLine(Self)) := InSource(Self)
      Pending(InLine(Self)) := false
      InMess(Self) := noMess
  endif


(*----------------------------------------------------------------------*)

(* for testing *)
transition R15a == 
      if MessInTr(n(maxQ),Home(InLine(Self))) = noMess 
      then  CCState(Self,InLine(Self)) := shared
      endif

(* original *)

transition R15 == 
  if InMess(Self) = inv
  then
      if MessInTr(n(maxQ),Home(InLine(Self))) = noMess 
      then  AppendToTransit (Home(InLine(Self)),(Self,invack,InSource(Self),InLine(Self)))  
            InMess(Self):=noMess
            if CCState(Self,InLine(Self)) = shared
            then CCState(Self,InLine(Self)) := invalid
            else if CurPhase(Self, InLine(Self)) = wait
                 then CurPhase(Self, InLine(Self)) := invalidPhase
                 endif
            endif
      endif
 endif


transition R16 == 
 if (InMess(Self) = invack and Home(InLine(Self)) = Self)
 then do forall agent_ in Agent_without_none with true
       if InSender(Self)=agent_
       then Sharer(InLine(Self),agent_) := false     
            if ( forall other_agent_ in (Agent_without_none\{agent_})
                 : Sharer(InLine(Self), other_agent_)=false )
            then if MessInTr(n(maxQ),InSource(Self)) = noMess
                 then AppendToTransit (InSource(Self), (Self,putx,InSource(Self),InLine(Self)))
                      Pending(InLine(Self)):=false
                      Owner(InLine(Self)) := InSource(Self) 
                      InMess(Self):=noMess
                 endif
            else InMess(Self):=noMess
            endif
        endif
       enddo
 endif


(*-------------------------------------------------------------*)

transition R17 == 
 if (InMess(Self) = rpl and Home(InLine(Self)) = Self)
 then if Sharer(InLine(Self),InSender(Self)) = true and Pending(InLine(Self)) = false       
      then Sharer(InLine(Self),InSender(Self)) := false
           CCState(Self,InLine(Self)) := invalid
      endif
      InMess(Self) := noMess
  endif

transition R18 == 
 if (InMess(Self) = wb and Home(InLine(Self)) = Self)
 then if Owner(InLine(Self)) != none
      then Owner(InLine(Self)) := none
           CCState(Self,InLine(Self)) := invalid
      endif
      InMess(Self) := noMess
  endif

(*-------------------------------------------------------------*)

transition behavior ==
  block
    R1_R2_R3_R4
    R5
    R6
    R7
    R8
    R7_R8
    R9
    R10
    R9_R10
    R11
    R12
    R13
    R14
    R13_R14
    R15
    R16 
    R17
    R18
  endblock

(*-------------------------------------------------------------*)

(* sending message means to write mess from transit into queue
   the message from transit has to be clear to indicate that 
   the sending is process (and has not failed!)
   if it is the case that sender is equal to destiny (Owner=sharedRequester)
   then InMess of sender should not be clear
   otherwise, it has to be cleared to indicate message has been send *)   

transition  ClearMessInTr(agent_) ==
block
  MessInTr(n(maxQ),agent_):=noMess    (* clear last entry in any case *)
  if MessInTr(n(2),agent_)=noMess        (* next message in transit after first *)
  then MessInTr(n(1),agent_):=noMess
  else do forall i in {2..maxQ}
        if MessInTr(n(i), agent_)!=noMess
        then MessInTr (n(i-1), agent_):=MessInTr(n(i), agent_)
             SenderInTr (n(i-1), agent_):=SenderInTr(n(i), agent_) 
             SourceInTr (n(i-1), agent_):=SourceInTr(n(i), agent_)
             LineInTr (n(i-1), agent_):=LineInTr(n(i), agent_)
(*             MessInTr (n(i), agent_):=noMess *) (* RACING MessInTr2 wird ueberschrieben!! *)
        else MessInTr(n(i-1), agent_):=noMess  (* wenn n(i) == noMess, dann loesche auch n(i-1) *)
        endif
       enddo
  endif
endblock

transition SendMess(agent_) ==
  block
   InSender(agent_):= SenderInTr(n(1), agent_) 
   InMess(agent_)  := MessInTr(n(1), agent_)  
   InSource(agent_):= SourceInTr(n(1), agent_)
   InLine(agent_)  := LineInTr(n(1), agent_) 
   ClearMessInTr(agent_)                   (* clear MessInTransit *)
  endblock


(* if a Request is send the MessInTransitRequest Variable is cleared
   and a new request can be adopted       *)
(* The guard for sending a request have to be satisfied when
   the request is passing through!! Not when the request is put into 
   Transit-Queue! *)


transition SendR(agent_) ==
  block
   InSender(agent_)  := SenderInTrR(agent_) 
   InMess(agent_)    := MessInTrR (agent_)  
   InSource(agent_)  := SourceInTrR (agent_)
   InLine(agent_)    := LineInTrR (agent_) 
   MessInTrR(agent_) := noMess            (* clear RequestInTransit *)
  endblock


transition SendRequest (agent_) ==
  if MessInTrR (agent_) = get 
     and CurPhase(SenderInTrR(agent_), LineInTrR (agent_)) = ready 
     and CCState(SenderInTrR(agent_), LineInTrR (agent_)) = invalid
  then SendR(agent_) 
       CurPhase(SenderInTrR(agent_), LineInTrR (agent_)) := wait
  else if MessInTrR (agent_) = getx
          and CurPhase(SenderInTrR(agent_), LineInTrR (agent_)) = ready 
          and CCState(SenderInTrR(agent_), LineInTrR (agent_)) = invalid
       then SendR(agent_) 
            CurPhase(SenderInTrR(agent_), LineInTrR (agent_)) := wait
       else if MessInTrR (agent_) = rpl
               and CurPhase(SenderInTrR(agent_), LineInTrR (agent_)) = ready 
               and CCState(SenderInTrR(agent_), LineInTrR (agent_)) = shared
            then SendR(agent_)
                 CCState(SenderInTrR(agent_), LineInTrR (agent_)) := invalid
            else if MessInTrR (agent_) = wb
                    and CurPhase(SenderInTrR(agent_), LineInTrR (agent_)) = ready 
                    and CCState(SenderInTrR(agent_), LineInTrR (agent_)) = exclusive
                 then SendR(agent_)
                      CCState(SenderInTrR(agent_), LineInTrR (agent_)) := invalid
                 endif
            endif
       endif
  endif


(*-- if there is a mess in transit then send
     only if there is no message in transit then send request 
     (this probably works only for non-intra-node comm!)  *)
(*-------------------------------------------------------------*)
(* do_forall version: problems in ki-opt-intermediate -> term2expr and simplify -> simplify_statics... *)

transition synchronize ==
 block
  do forall agent_ in Agent_without_none with true
    if InMess(agent_)=noMess
    then if MessInTr(n(1),agent_) != noMess
         then SendMess(agent_)
         else if MessInTrR(agent_) != noMess and InMess(agent_)=noMess  (* MessInTrR ohnehin nur an Owner! *)
              then SendRequest(agent_)
              endif
         endif
    endif
  enddo
 endblock

(*-------------------------------------------------------------*)

transition main ==
   if toggle=behave
    then 
       behavior
       toggle:=sync
   else 
       synchronize
       toggle:=behave
   endif