--- July, 19

mod PSCONFIGURATION is
  pr QID .
  sorts Obj Dissolve InTarget OutTarget OutMessage Message .
  sorts Soup OutSoup DissSoup OutDissSoup MsgDissSoup Soup? .
  subsort Obj < Soup < Soup? .
  subsort Dissolve Soup < DissSoup < OutDissSoup < MsgDissSoup < Soup? .
  subsort OutMessage Soup < OutSoup < OutDissSoup .
  subsort OutMessage < Message .
  subsort Message DissSoup < MsgDissSoup < Soup? .

  sorts Membrane DMembrane Membrane+ Membrane? .
  sorts MembraneSet DMembraneSet MembraneSet+ MembraneSet? . 
  sorts EmptyMembraneSet NeMembraneSet NeDMembraneSet NeMembraneSet+ 
        NeMembraneSet? .
  sorts Configuration IConfiguration Configuration? .
  sort Label . subsort Label < Qid .
  subsort Configuration IConfiguration < Configuration? .
  subsort Membrane < DMembrane < Membrane+ < Membrane? .
  subsort EmptyMembraneSet < MembraneSet .
  subsort MembraneSet < DMembraneSet < MembraneSet+ < MembraneSet? .
  subsort Membrane < NeMembraneSet < MembraneSet .
  subsort DMembrane < NeDMembraneSet < DMembraneSet .
  subsort Membrane+ < NeMembraneSet+ < MembraneSet+ .
  subsort Membrane? < NeMembraneSet? < MembraneSet? .
  subsort NeMembraneSet < NeDMembraneSet < NeMembraneSet+ < NeMembraneSet? .

  op empty : -> Soup .
  op __ : Soup? Soup? -> Soup? [assoc comm id: empty] .
  op __ : Soup Soup -> Soup [assoc comm id: empty] .
  op __ : OutSoup OutSoup -> OutSoup [assoc comm id: empty] .
  op __ : DissSoup DissSoup -> DissSoup [assoc comm id: empty] .
  op __ : OutDissSoup OutDissSoup -> OutDissSoup [assoc comm id: empty] .
  op __ : MsgDissSoup MsgDissSoup -> MsgDissSoup [assoc comm id: empty] .

  op delta : -> Dissolve .
  eq delta delta = delta .

  op in : Label -> InTarget .
  op out : -> OutTarget .
  op `(_`,_`) : Soup InTarget -> Message .
  op `(_`,_`) : Soup OutTarget -> OutMessage .

  op `{_`} : Membrane -> Configuration .
  op `{_`} : Membrane? -> Configuration? .

  op empty : -> EmptyMembraneSet .

  op <_|_> : Label Soup -> Membrane .
  op _`,_ : NeMembraneSet NeMembraneSet -> 
            NeMembraneSet [assoc comm id: empty] .
  op _`,_ : MembraneSet NeMembraneSet -> NeMembraneSet [assoc comm id: empty] .
  op _`,_ : MembraneSet MembraneSet -> MembraneSet [assoc comm id: empty] .
  op <_|_;_> : Label Soup MembraneSet -> Membrane .

  op <_|_> : Label DissSoup -> DMembrane .
  op _`,_ : NeDMembraneSet NeDMembraneSet -> 
            NeDMembraneSet [assoc comm id: empty] .
  op _`,_ : DMembraneSet NeDMembraneSet -> 
            NeDMembraneSet [assoc comm id: empty] .
  op _`,_ : DMembraneSet DMembraneSet -> DMembraneSet [assoc comm id: empty] .
  op <_|_;_> : Label DissSoup NeDMembraneSet -> DMembrane .

  op <_|_> : Label MsgDissSoup -> Membrane+ .
  op _`,_ : NeMembraneSet+ NeMembraneSet+ -> 
            NeMembraneSet+ [assoc comm id: empty] .
  op _`,_ : MembraneSet+ NeMembraneSet+ -> 
            NeMembraneSet+ [assoc comm id: empty] .
  op _`,_ : MembraneSet+ MembraneSet+ -> MembraneSet+ [assoc comm id: empty] .
  op <_|_;_> : Label MsgDissSoup MembraneSet+ -> Membrane+ .

  op <_|_> : Label Soup? -> Membrane? .
  op _`,_ : NeMembraneSet? NeMembraneSet? -> 
            NeMembraneSet? [assoc comm id: empty] .
  op _`,_ : MembraneSet? NeMembraneSet? -> 
            NeMembraneSet? [assoc comm id: empty] .
  op _`,_ : MembraneSet? MembraneSet? -> MembraneSet? [assoc comm id: empty] .
  op <_|_;_> : Label Soup? MembraneSet? -> Membrane? .

endm