Z-spec for Petri-net ADT Paul Rademacher Kenny Hoff Dave McAllister ************************************************** Given sets and globals constants ************************************************** The specification has the following given sets: * PLACE - set of places * TRANS - set of transitions The following definition given the values that an operation may return: Response ::= ok | nonexist_arc | nonexist_place | already_exists | nonexist | full | notready ********************************************* Component Definitions ********************************************* +- pnet --------------------- | trans : P TRANS | places : P PLACE | num_p, max_p : N | num_t, max_t : N | arc_o : PLACE |--> TRANS /* Arcs out of a place */ | arc_i : TRANS |--> PLACE /* Arc into a place */ | +-------------------- | dom(arc_o) is subset of places | /* not all places have an ougoing arc */ | range(arc_o) is subset trans | /* not all trans have an incoming arc */ | | dom(arc_i) is subset of trans | /* not all trans have an outgoing arc */ | range(arc_i) is subset of places | /* not all places have an incoming arc */ | +------------------------------ +- places -------------------- | token_cnt : N /* number of tokens in place */ | +-------------------- | +------------------------------ +- trans -------------------- | | +-------------------- | +------------------------------ ************************************************** Initialization ************************************************** +- Init_pnet --------------------- | delta pnet | +-------------------- | trans = NULL | places = NULL | max_p = 0 | num_p = 0 | max_t = 0 | num_t = 0 +--------------------------------- +- Init_places -------------------- | delta places | +-------------------- | token_cnt = 0 +--------------------------------- +- Init_trans -------------------- | | +-------------------- | +--------------------------------- ************************************************** Operations ************************************************** ****************************** Generic add_arc ops ****************************** +- Add_arc() -------------------- | delta pnet | p? : PLACE | t? : TRANS | r! : Response | +-------------------- | +-------------------------------- +- Add_arc_nonexist_place ----- | Add_arc() | +-------------------- | p? is not an element of place | r! = nonexist_place +--------------------------------- +- Add_arc_nonexist_trans ----- | Add_arc() | +-------------------- | t? is not an element of trans | r! = nonexist_trans +--------------------------------- ****************************** specific Add_arc_in ops ****************************** +- Add_arc_in_ok ---------------- | Add_arc() | +-------------------- | p? is element of place | t? is element of trans | {t? |--> p?} is not in the relation arc_i | arc_i' = arc_i UNION {t? |--> p?} | r! = ok +----------------------------- +- Add_arc_in_exists ------------ | Add_arc() | +-------------------- | {t? |--> p?} is in the relation arc_i | r! = already_exists +-------------------------------- Now the complete Add_arc_in is defined as: Add_arc_in ^= Add_arc_in_ok or Add_arc_in_exists or Add_arc_nonexist_place or Add_arc_nonexist_trans ****************************** specific Add_arc_out ops ****************************** +- Add_arc_out_ok --------------- | Add_arc() | +-------------------- | p? is element of place | t? is element of trans | {p? |--> t?} is not in the relation arc_o | arc_o' = arc_o UNION {p? |--> t?} | r! = ok +--------------------------------- +- Add_arc_out_exists ------------ | Add_arc() | +-------------------- | {p? |--> t?} is in the relation arc_o | r! = already_exists +--------------------------------- Add_arc_out ^= Add_arc_out_ok or Add_arc_out_exists or Add_arc_nonexist_place or Add_arc_nonexist_trans ****************************** generic Delete_arc ops ****************************** +- Delete_arc() -------------------- | delta pnet | p? : PLACE | t? : TRANS | r! : Response | +-------------------- | +-------------------------------- +- Delete_arc_nonexist_place ----- | Delete_arc() | +-------------------- | p? is not an element of place | r! = nonexist_place +--------------------------------- +- Delete_arc_nonexist_trans ----- | Delete_arc() | +-------------------- | t? is not an element of trans | r! = nonexist_trans +--------------------------------- ****************************** specific Delete_arc_in ops ****************************** +- Delete_arc_in_ok ---------------- | Delete_arc() | +-------------------- | p? is element of place | t? is element of trans | {t? |--> p?} is in the relation arc_i | arc_i' = arc_i \ {t? |--> p?} | r! = ok +----------------------------- +- Delete_arc_in_nonexist ------------ | Delete_arc() | +-------------------- | {t? |--> p?} is not in the relation arc_i | r! = already_exists +-------------------------------- Delete_arc_in ^= Delete_arc_in_ok or Delete_arc_in_nonexist or Delete_arc_nonexist_place or Delete_arc_nonexist_trans ****************************** specific Delete_arc_out ops ****************************** +- Delete_arc_out_ok ---------------- | Delete_arc() | +-------------------- | p? is element of place | t? is element of trans | {p? |--> t?} is in the relation arc_o | arc_o' = arc_o \ {p? |--> t?} | r! = ok +------------------------------------- +- Delete_arc_out_nonexist ------------ | Delete_arc() | +-------------------- | {p? |--> t?} is not in the relation arc_o | r! = already_exists +--------------------------------------- Delete_arc_out ^= Delete_arc_out_ok or Delete_arc_out_nonexist or Delete_arc_nonexist_place or Delete_arc_nonexist_trans ****************************** Add_place ops ****************************** +- Add_place_ok --------------- | delta pnet | p? : PLACE | r! : Response | +-------------------- | p? is not an element of places | num_p < max_p | num_p' = num_p + 1 | places = places UNION p? | r! = ok +------------------------------ +- Add_place_full ------------ | pnet | p? : PLACE | r! : Response | +-------------------- | num_p = max_p | r! = full +------------------------------ +- Add_place_already_exists ------------ | pnet | p? : PLACE | r! : Response | +-------------------- | p? is an element of places | r! = already_exists +------------------------------ Add_place ^= Add_place_ok or Add_place_full or Add_place_already_exists ****************************** Delete_place ops ****************************** +- Delete_place_ok --------------- | delta pnet | p? : PLACE | r! : Response | +-------------------- | p? is an element of place | num_p' = num_p - 1 | places = places \ p? | r! = ok +------------------------------ +- Delete_place_nonexist ------------ | pnet | p? : PLACE | r! : Response | +-------------------- | p? is NOT an element of place | r! = nonexist +------------------------------ Delete_place ^= Delete_place_ok or Delete_place_nonexist ****************************** Add_trans ops ****************************** +- Add_trans_ok --------------- | delta pnet | t? : TRANS | r! : Response | +-------------------- | num_t < max_t | num_t' = num_t + 1 | trans = trans UNION t? | r! = ok +------------------------------ +- Add_trans_full ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | num_t = max_t | r! = full +------------------------------ +- Add_trans_exists ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t? is an element of trans | r! = already_exists +------------------------------ Add_trans ^= Add_trans_ok or Add_trans_full or Add_trans_exists ****************************** Delete_trans ops ****************************** +- Delete_trans_ok --------------- | delta pnet | t? : TRANS | r! : Response | +-------------------- | t? is an element of trans | num_t' = num_t - 1 | trans = trans \ t? | r! = ok +------------------------------ +- Delete_trans_nonexist ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t? is NOT an element of trans | r! = nonexist +------------------------------ Delete_trans ^= Delete_trans_ok or Delete_trans_nonexist ****************************** Enable_trans ops ****************************** +- Enabled_trans_ok ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t? is an element of trans | for all a in arcs_o such that range(a)==t?, | dom(a).token_cnt > 0 | r! = ok +------------------------------ +- Enabled_trans_notready ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t is an element of trans | there exists a in arcs_o such that | (range(a)==t AND dom(a).token_cnt==0) | r! = notready +------------------------------ +- Enabled_trans_nonexist ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t? is NOT an element of trans | r! = nonexist +------------------------------ Enabled_trans ^= Enabled_trans_ok or Enabled_trans_notready or Enabled_trans_nonexist ****************************** Fire_trans ops ****************************** +- Fire_trans_ok ------------ | delta pnet | t? : TRANS | r! : Response | +-------------------- | t? is an element of trans | for all a in arcs_o such that range(a)==t?, | dom(a).token_cnt > 0 | for all a in arcs_o such that range(a)==t?, | dom(a).token_cnt' = dom(a).token_cnt - 1 | for all a in arcs_i such that dom(a)==t?, | range(a).token_cnt' = range(a).token_cnt + 1 | r! = ok +------------------------------ +- Fire_trans_notready ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t? is an element of trans | there exists a in arcs_o such that | (range(a)==t? AND dom(a).token_cnt==0) | r! = notready +------------------------------ +- Fire_trans_nonexist ------------ | pnet | t? : TRANS | r! : Response | +-------------------- | t? is NOT an element of trans | r! = nonexist +------------------------------ Fire_trans ^= Fire_trans_ok or Fire_trans_notready or Fire_trans_nonexist