bag.mch

这里几个源代码是用BToolkit软件写的。这是关于一些操作

MACHINE           Bag(ELEM,cap)	  

CONSTANTS 	  AMOUNT

PROPERTIES        AMOUNT=0..cap

VARIABLES         bag, elem

INVARIANT         bag : ELEM<->AMOUNT& elem<:ELEM & dom(bag)=elem

INITIALISATION    bag := {}

OPERATIONS

  addbag(ee:ELEM )=
		IF ee /:dom(bag)
		THEN elem := elem \/ {ee} ||
		     bag:= bag\/ {ee |->1}
		ELSE 
		     bag(ee) := bag(ee)+1
		END;

  rembag(ee:ELEM )=
		PRE bag /= {}&ee :dom(bag)
		THEN
			IF bag(ee)=1
			THEN elem := elem - {ee} ||
			     bag:= {ee}<<|bag
			ELSE 
			     bag(ee) := bag(ee)-1
			END
		END;
  oo<--countelm(ee:ELEM)=
		IF ee :dom(bag)
		THEN oo := bag(ee)
		ELSE oo := 0
		END;

  oo<--totelms=
		IF bag /={}
		THEN oo := SIGMA(elm).(elm:dom(bag) |bag(elm))
		ELSE oo :=0
		END;
		
  bb<--isin(ee:ELEM)=
		IF ee :dom(bag)
		THEN bb := 1
		ELSE bb := 0
		END
/*  bagunion(bb<:bag) */
		
END