ALGEBRA SET

sorts (a set)

cons
    Set : (a list) -> (a set)

funs
    Remove       : a set * a     -> a set
    Union        : a set * a set -> a set
    Intersection : a set * a set -> a set
    IsEmpty      : a set         -> bool
    NotIn        : a * a set     -> bool
    In           : a * a set     -> bool

syntax 
    Set is emptylist "{" "," "}"

    Remove 	is infix "diff" right 21
    Union 	is infix "U" left 60
    Intersection is infix "^" left 60
    IsEmpty 	is prefix "isempty"
    NotIn 	is infix "notin" left 10
    In 		is infix "member" left 10
end


ALGEBRA STRL_SIGNAL

sorts  signal relabeling strl_relation

cons
        Relabeling : signal * signal -> relabeling
	ExclRel :    signal list     -> strl_relation
	ImplRel :    signal * signal -> strl_relation

funs
        RelSort  : strl_relation -> (signal set)

syntax
        Relabeling  	is infix    "/"	left 10
	ExclRel 	is nonemptylist "{{" "#" "}}"
	ImplRel 	is infix "=>"		left 20
        RelSort 	is prefix  "relsort"

end

ALGEBRA STRL_SIGNAL_SET

imports SET

funs
	HideSig : (signal set) * signal            -> (signal set)
        Relabel : (signal set) * (relabeling list) -> (signal set)

syntax
	HideSig  is infix "hidesig"	left 10
        Relabel  is infix "rename"	left 10
end


ALGEBRA STRL_ACTION

imports SET STRL_SIGNAL

sorts   action

cons    
        Tau         : action
	Exit        : signal
        Atom        : signal                      -> action
        Received    : signal                      -> action
        Absent      : signal                      -> action
        Emitted     : signal                      -> action
        Comp        : action * action -> action




funs    
        IsTerminal     : action                     -> bool
        IsNotTerminal  : action                     -> bool
        Hiding         : action * signal             -> action
        ApplyRenaming  : action * (relabeling list) -> action
        ApplySimplRel : action * strl_relation      -> action
        ApplyComplRel : action * strl_relation      -> action

syntax  
        Tau                   is "tau"
	Exit                  is "exit_"
        Atom(s)               is "s"
	Absent(s)             is "s #"
	Emitted (s)           is "s !"
	Received (s)          is "s ?"
        Comp                  is infix "."   		left 20
        
        IsTerminal            is prefix   "isterminal"
        IsNotTerminal         is prefix   "isnotterminal"
        Hiding		      is infix   "hiding"	left 10
	ApplyRenaming (a,l)   is "a < l >"
        ApplySimplRel(a,r)    is "simplAct r in a " 
        ApplyComplRel(a,r)    is "complAct r in a "

priorities
   right 31 "<"
   right 11 "#" "?" "!"
end

ALGEBRA STRL_PREDICATE

imports SET STRL_ACTION

funs
        Divides     : action * action          -> bool
        Equal       : action * action          -> bool
        Different   : action * action          -> bool
        Compatible  : action * action          -> bool
        Restriction : action * signal          -> bool
        CheckRel   : strl_relation * action	       -> bool

syntax
       Divides             is infix    "divides"	left 20
       Equal               is infix    "="		left 10
       Different           is infix    "<>"		left 10
       Compatible          is infix    "compatible"	left 20
       Restriction         is infix    "restriction"	right 15 
       CheckRel (r,a)      is "check r in a end"   
end

ALGEBRA STRL

imports SET STRL_SIGNAL STRL_ACTION

sorts 
        process
cons
        Error              : process
	Nothing            : process
	Halt               : process
        Stop               : process
	Emit               : signal                      -> process
        Await              : signal                      -> process
	Present            : signal * process * process  -> process
        WatchingImmediate  : process * process           -> process
	Watching           : process * process           -> process
	Sequence           : process * process           -> process
	Parallel           : process * process           -> process
        LocalSignal        : process * signal             -> process
        Renaming           : process * (relabeling list) -> process
        ComplRel           : strl_relation * process      -> process
        SimplRel           : strl_relation * process      -> process

syntax
        Error              is     "??"
	Nothing            is     "nothing"
	Halt               is     "halt"
        Stop               is     "stop"
        Await              is prefix   "await"
	Emit               is prefix   "emit"
	Present(s,t1,t2)   is 	  "present s then t1 else t2 end"
  	WatchingImmediate(p1,p2)  is "watching immediate p2 do p1 end"
	Watching(p1,p2)    is "watching p2 do p1 end"
	Sequence           is infix    ">>"        left 40
	Parallel           is infix    "//"       left 10
        LocalSignal(p,s)   is "localsignal s in p end"
        Renaming (p,l)     is "p [ l ]"
        ComplRel(r,p)      is "compl r in p"
        SimplRel(r,p)      is "simpl r in p"

priorities
    right 31 "["

end

SEMANTICS STRL_SEM

imports STRL_ACTION STRL

funs
	Transition : process * action * process -> bool
        Sort :       process * (signal set)     -> bool
        Halting:     process                    -> bool
syntax
	Transition(p,a,q) is "p -- a --> q"
        Sort(p,s)         is "sort ( p , s )"
        Halting(p)        is "p V"

conventions
	agent is process
	transitions is Transition
end