ALGEBRA SET

sorts (a set)

cons
    ExprSet : a list -> a set

funs
    IsEmpty : a set -> bool
    Member : a * a set -> bool

syntax 
    IsEmpty is prefix "isempty"
    Member is infix "member" left 10

    ExprSet is emptylist "{" "," "}"
end

ALGEBRA BLOTOS_AA

imports SET

sorts action

cons
    Internal : action
    Delta :  action

funs
    Equal : action * action -> bool

syntax 
    Internal is "i"
    Delta is "delta"

    Equal is infix "equal" left 10

end

ALGEBRA BLOTOS_OP

imports BLOTOS_AA SET

sorts process

cons
  Stop : process
  Exit : process
  Prefixing : action * process -> process
  Hiding : (action set) * process -> process
  Choice : process * process -> process
  Parallel : process * process -> process
  RDV : process * action set * process -> process
  Disable : process * process -> process
  Enable : process * process -> process

syntax
  Stop 		is "stop"
  Exit 		is "exit"
  Prefixing 	is infix ";" left 30
  Hiding(S,p) 	is "hide S in p" 
  Choice 	is infix "[]" left 40
  Parallel 	is infix "||" left 60
  RDV(p1,s,p2)	is "p1 // s // p2"
  Disable 	is infix "[>" left 80
  Enable 	is infix ">>" left 80

priorities
  left 60 "//"

conventions
  agent is process
end

ALGEBRA FUNCT

sorts funct
cons
  NoExit : funct
  YesExit : funct
syntax
  NoExit is "noexit"
  YesExit is "yesexit"
end

SEMANTICS BLOTOS_SEM

imports BLOTOS_OP FUNCT

funs
  Functionality : process * funct -> bool
  Transition : process * action * process -> bool

inputs
  Functionality (p,f) is p
  Transition (p,a,q) is p

syntax
  Functionality is infix "-:" left 2
  Transition(p,a,q) is "p -- a --> q"

end