*** sets of data (proxy descriptions) and strings (svcnames, ids)
fmod ATTACKER-AUX is
  inc STRING .
  inc DATA .
  sort StringSet .
  subsort String < StringSet .
  op none : -> StringSet .
  op __ : StringSet StringSet -> StringSet [assoc comm id: none] .
  op member : String StringSet -> Bool .
  eq member(q:String, none) = false .
  eq member(q:String, qq:String qs:StringSet) = 
     if (q:String == qq:String)
     then true
     else member(q:String, qs:StringSet)
     fi .
  op addElt : String StringSet -> StringSet .
  eq addElt(q:String, qs:StringSet) =
      if ( member(q:String, qs:StringSet) )
      then qs:StringSet
      else (q:String qs:StringSet)
      fi .

  sort DataSet .
  subsort Data < DataSet .
  op none : -> DataSet .
  op __ : DataSet DataSet -> DataSet [assoc comm id: none] .
  op member : DataX DataSet -> Bool .
  eq member(dx:DataX, none) = false .
  eq member(dx:DataX, dd:Data ds:DataSet) = 
     if (dx:DataX == dd:Data)
     then true
     else member(dx:DataX, ds:DataSet)
     fi .

  op addElt : DataX DataSet -> DataSet .
  eq addElt(dx:DataX, ds:DataSet) =
      ( if not(dx:DataX :: Data)
        then ds:DataSet
        else ( if member(dx:DataX, ds:DataSet)
        then ds:DataSet
        else (dx:DataX ds:DataSet)
        fi )
      fi )
  .

endfm

