Commit f1b3035d authored by Ocan Sankur's avatar Ocan Sankur

Fixed extrapolation bug

parent 4445daee
......@@ -57,7 +57,6 @@ module WSTS_WO (Key : Hashtbl.HashedType)
struct
module KeyHashtbl = Hashtbl.Make(Key)
type dbm_list = BDbm.Dbm.t list ref
type key = KeyHashtbl.key
(* cf. WALK_ORDER signature *)
......
......@@ -25,6 +25,8 @@ sig
val to_string : t -> string
val _internal_addr : t -> int
(* a function that compares two DBMs and tells which one is best to explore first *)
val is_best : t -> t -> int
end
......@@ -37,6 +39,8 @@ sig
val from_dbm : dbm_t -> t
val hash : t -> int
val create : int -> t
val dimension : t -> int
val is_empty : t -> bool
val set_empty : t -> unit
val add_dbm : t -> dbm_t -> unit
......@@ -96,7 +100,7 @@ struct
let to_dbm t =
let res = ref [] in
iter t (fun z -> res := (Dbm.copy z) :: !res);
iter t (fun z -> res := z :: !res);
!res
let intersect t z = intersect_dbm t z
......@@ -129,11 +133,14 @@ struct
let is_best z1 z2 = compare (infimum z1) (infimum z2)
let _internal_addr t = 0
end
and Fed : FED =
struct
include Udbml_priced.PFed
let dimension _ = failwith "dimension pfed"
let to_dbm t =
let res = ref [] in
iter t (fun z -> res := z :: !res);
......
......@@ -4,6 +4,20 @@ open Varcontext
open Printf
open Dbm
(** Utility functions which should be replaced with some extended library *)
exception Found
let queue_exists f q=
try
Queue.iter (fun y -> if f y then raise Found) q;
false
with Found -> true
let queue_filter f q=
let q' = Queue.create () in
Queue.iter (fun y -> if f y then Queue.add y q') q;
Queue.clear q;
Queue.iter (fun y -> Queue.add y q) q'
let print_path = ref false
(** An abstract type for zone abstractions *)
......@@ -37,6 +51,11 @@ struct
let extrapolate zone (ta, loc) =
let (lbounds, ubounds) = TA.lu_bounds ta loc in
(*
printf "LU bounds for state: ";
TA.print_discrete_state stdout ta loc;
printf "\n>> %s\n>> %s\n" (Udbml.Carray.to_string lbounds) (Udbml.Carray.to_string ubounds);
*)
Udbml_unpriced.Dbm.extrapolate_lu_bounds zone lbounds ubounds
end
......@@ -207,7 +226,7 @@ end
(** Builds an effective walk order, given a WAIT_CONTAINER and an INCLUSION.
*)
module Walk_Order (ContFun : WAIT_CONTAINER)
module Walk_Order (WaitContFun : WAIT_CONTAINER)
(Key : Hashtbl.HashedType)
(BDbm : Dbm.BIG_IDBM)
(COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
......@@ -217,53 +236,55 @@ struct
module KeyHashtbl = Hashtbl.Make(Key)
type dbm_list = BDbm.Dbm.t list ref
(* type dbm_list = BDbm.Dbm.t list ref*)
type dbm_list = BDbm.Dbm.t Queue.t
type key = KeyHashtbl.key
(* cf. WALK_ORDER signature *)
type path = key _path
module Cont = ContFun(Best)
module WaitCont = WaitContFun(Best)
type t = dbm_list KeyHashtbl.t * Cont.t
type t = dbm_list KeyHashtbl.t * WaitCont.t
let create () = (KeyHashtbl.create 1024, Cont.create ())
let create () = (KeyHashtbl.create 1024, WaitCont.create ())
let find_or_add : dbm_list KeyHashtbl.t -> key -> dbm_list =
fun h -> fun x ->
try KeyHashtbl.find h x
with Not_found ->
incr Stats.number_of_discrete_states;
let y = ref [] in
let y = Queue.create () in
KeyHashtbl.add h x y;
y
let add_to_waiting _ (_, waiting) s = Cont.push s waiting
let add_to_waiting _ (_, waiting) s = WaitCont.push s waiting
let is_in_passed comp (passed, _) (l, z, a) =
let bucket = find_or_add passed l in
List.exists (fun x -> comp a z x) !bucket
queue_exists (fun x -> comp a z x) bucket
let add_to_passed comp (passed, waiting) (l, z, a) =
(* TODO it is the responsibility of the Stats module to print stat infos *)
(* TODO it is the responsibility of the Stats module to print stat infos *)
incr Stats.states_explored;
if ((!Stats.states_explored mod Stats.modulo) = 0) then (
Printf.printf "we have explored %d states, %d in the waiting list\r" !Stats.states_explored (Cont.length waiting);
Printf.printf "we have explored %d states, %d in the waiting list\r" !Stats.states_explored (WaitCont.length waiting);
flush stdout
);
let bucket = find_or_add passed l in
let old_size = List.length !bucket in
let old_size = Queue.length bucket in
let is_incomp x = not (comp a x z) in
bucket := z :: (List.filter is_incomp !bucket);
queue_filter is_incomp bucket;
Queue.add z bucket;
incr Stats.states_seen;
if (old_size < List.length !bucket) then
Stats.max_states := !Stats.max_states - old_size + List.length !bucket
if (old_size < Queue.length bucket) then
Stats.max_states := !Stats.max_states - old_size + Queue.length bucket
let get_next (_, waiting) = Cont.pop waiting
let get_next (_, waiting) = WaitCont.pop waiting
let is_done (_, waiting) = Cont.is_empty waiting
let is_done (_, waiting) = WaitCont.is_empty waiting
let waiting_length (_, waiting) = Cont.length waiting
let waiting_length (_, waiting) = WaitCont.length waiting
let clean pred (passed, waiting) =
let size_before = ref 0 in
......@@ -274,9 +295,9 @@ struct
if (res) then incr size_after;
res
in
KeyHashtbl.iter (fun _ -> fun bucket -> bucket := List.filter predaux !bucket;) passed;
KeyHashtbl.iter (fun _ -> fun bucket -> queue_filter predaux bucket) passed;
Printf.printf "cleaning: shrink from %d states to %d states stored\n" !size_before !size_after;
Printf.printf "still %d states waiting for treatment\n" (Cont.length waiting);
Printf.printf "still %d states waiting for treatment\n" (WaitCont.length waiting);
flush stdout
end
......@@ -422,7 +443,12 @@ struct
if (Fed.is_empty result_zone) then
succs_list
else (
Fed.iter result_zone (fun z -> ABS.extrapolate z (ta, target));
let result_zone' = Fed.create (Fed.dimension result_zone) in
Fed.iter result_zone (fun z ->
ABS.extrapolate z (ta, target);
Fed.add_dbm result_zone' (Dbm.copy z)
);
let result_zone = result_zone' in
let new_path = (source, guard, resets, target) :: path in
if (TA.is_urgent_or_committed ta target) then
let tmp = ref [] in
......@@ -470,8 +496,8 @@ struct
ABS.extrapolate z (ta, init);
WO.add_to_waiting dbm_comp wot (init, z, COMP.get_arg ta init, [])
) (Fed.to_dbm initfed);
walk_aux dbm_comp wot (succ_zone ta) update_result res0
let result = walk_aux dbm_comp wot (succ_zone ta) update_result res0 in
result
(* a helper function to turn a path into a string *)
let path_to_string ta path =
......
......@@ -625,7 +625,7 @@ struct
(* TODO some clocks already have their constant known, cache them *)
let _lubounds ta state =
let n = VarContext.size ta.clocks in
let lb, ub = Array.make n 0, Array.make n 0 in
let lb, ub = Array.make n (-Udbml.Basic_types.infty), Array.make n (-Udbml.Basic_types.infty) in
let eval = eval_exp ta state.stateVars in
for cl=1 to n-1 do
Array.iter
......
......@@ -14,6 +14,7 @@ struct
let pop = Stack.pop
let is_empty = Stack.is_empty
let length = Stack.length
let iter = Stack.iter
end
(**
......@@ -30,11 +31,12 @@ struct
let pop = Queue.pop
let is_empty = Queue.is_empty
let length = Queue.length
let iter = Queue.iter
end
module Walk_DFS = Walk_Order_Opt (WOStack)
module Walk_BFS = Walk_Order_Opt (WOQueue)
module Walk_BFS = Walk_Order (WOQueue)
(**
* A custom tree to represent sorted sets, with inplace insertion.
......@@ -42,7 +44,7 @@ module Walk_BFS = Walk_Order_Opt (WOQueue)
*)
module MyBTree (T : sig val threshold : int end) : WAIT_CONTAINER =
functor (Elem : WaitOrderedType) ->
struct
struct
type btree =
Null
| Node of treenode
......
E<> ( P1.error and P2.sender_transm)
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// CSMA/CD 9
// Carrier Sense, Multiple-Access with Collision Detection
//
// automatically generated by script genCSMA_CD.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 19 11:48:20 2001
// ------------------------------------------------------------
chan begin, end, busy, cd1;</declaration><template><name>P0</name><declaration>clock x;</declaration><location id="id0" x="-120" y="80"><name x="-192" y="48">bus_idle</name></location><location id="id1" x="48" y="80"><name x="24" y="-8">bus_active</name></location><location id="id2" x="208" y="80"><name x="176" y="0">bus_collision1</name><label kind="invariant" x="176" y="24">x &lt;= 26</label></location><init ref="id0"/><transition><source ref="id2"/><target ref="id0"/><label kind="guard" x="40" y="176">x &lt;= 26</label><label kind="synchronisation" x="40" y="191">cd1 !</label><label kind="assignment" x="40" y="206">x=0</label><nail x="96" y="232"/><nail x="32" y="232"/></transition><transition><source ref="id0"/><target ref="id1"/><label kind="synchronisation" x="-72" y="40">begin ?</label><label kind="assignment" x="-72" y="56">x= 0</label></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="120">end ?</label><label kind="assignment" x="-40" y="136">x= 0</label><nail x="48" y="112"/><nail x="-120" y="112"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="guard" x="24" y="-24">x &gt;= 26</label><label kind="synchronisation" x="24" y="8">busy !</label><nail x="16" y="32"/><nail x="80" y="32"/></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="112" y="48">x &lt;= 26</label><label kind="synchronisation" x="112" y="88">begin ?</label><label kind="assignment" x="112" y="104">x= 0</label></transition></template><template><name>P1</name><declaration>clock x;</declaration><location id="id3" x="344" y="-24"><name x="334" y="-54">error</name></location><location id="id4" x="-48" y="72"><name x="-120" y="16">sender_wait</name></location><location id="id5" x="192" y="80"><name x="216" y="64">sender_transm</name><label kind="invariant" x="208" y="80">x&lt;= 808</label></location><location id="id6" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="180" y="245">x &lt;= 52</label></location><init ref="id4"/><transition><source ref="id5"/><target ref="id3"/><label kind="guard" x="224" y="0">x&gt;=53</label></transition><transition><source ref="id4"/><target ref="id5"/><label kind="synchronisation" x="32" y="-32">begin !</label><label kind="assignment" x="56" y="0">x= 0</label><nail x="80" y="-16"/></transition><transition><source ref="id4"/><target ref="id4"/><label kind="synchronisation" x="-108" y="57">cd1 ?</label><label kind="assignment" x="-108" y="72">x= 0</label><nail x="-78" y="42"/><nail x="-18" y="42"/></transition><transition><source ref="id4"/><target ref="id6"/><label kind="synchronisation" x="55" y="140">cd1 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id4"/><target ref="id6"/><label kind="synchronisation" x="55" y="140">busy ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id5"/><target ref="id4"/><label kind="guard" x="96" y="80">x == 808</label><label kind="synchronisation" x="64" y="64">end !</label><label kind="assignment" x="55" y="80">x= 0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="312" y="144">x &lt;= 52</label><label kind="synchronisation" x="264" y="144">cd1 ?</label><label kind="assignment" x="130" y="155">x= 0</label><nail x="264" y="152"/></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="160" y="144">begin !</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id6"/><target ref="id6"/><label kind="guard" x="130" y="200">x &lt;= 52</label><label kind="synchronisation" x="130" y="215">cd1 ?</label><label kind="assignment" x="130" y="230">x= 0</label><nail x="160" y="200"/><nail x="220" y="200"/></transition></template><system>system P0, P1;</system></nta>
\ No newline at end of file
E<> ( P1.error and P2.sender_transm)
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// CSMA/CD 9
// Carrier Sense, Multiple-Access with Collision Detection
//
// automatically generated by script genCSMA_CD.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 19 11:48:20 2001
// ------------------------------------------------------------
chan begin, end, busy, cd1, cd2, cd3, cd4, cd5, cd6, cd7, cd8, cd9;</declaration><template><name>P0</name><declaration>clock x;</declaration><location id="id0" x="-120" y="80"><name x="-192" y="48">bus_idle</name></location><location id="id1" x="48" y="80"><name x="24" y="-8">bus_active</name></location><location id="id2" x="208" y="80"><name x="176" y="0">bus_collision1</name><label kind="invariant" x="176" y="24">x &lt;= 26</label></location><location id="id3" x="344" y="80"><name x="334" y="50">bus_collision2</name><label kind="invariant" x="360" y="72">x &lt;= 0</label></location><init ref="id0"/><transition><source ref="id3"/><target ref="id0"/><label kind="guard" x="44" y="210">x&lt;=0</label><label kind="synchronisation" x="44" y="225">cd2!</label><label kind="assignment" x="44" y="240">x=0</label><nail x="96" y="272"/><nail x="-40" y="272"/></transition><transition><source ref="id0"/><target ref="id1"/><label kind="synchronisation" x="-72" y="40">begin ?</label><label kind="assignment" x="-72" y="56">x= 0</label></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="120">end ?</label><label kind="assignment" x="-40" y="136">x= 0</label><nail x="48" y="112"/><nail x="-120" y="112"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="guard" x="24" y="-24">x &gt;= 26</label><label kind="synchronisation" x="24" y="8">busy !</label><nail x="16" y="32"/><nail x="80" y="32"/></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="112" y="48">x &lt;= 26</label><label kind="synchronisation" x="112" y="88">begin ?</label><label kind="assignment" x="112" y="104">x= 0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="272" y="25">x &lt;= 26</label><label kind="synchronisation" x="272" y="40">cd1 !</label><label kind="assignment" x="272" y="55">x= 0</label></transition></template><template><name>P1</name><declaration>clock x;</declaration><location id="id4" x="344" y="-24"><name x="334" y="-54">error</name></location><location id="id5" x="-48" y="72"><name x="-120" y="16">sender_wait</name></location><location id="id6" x="192" y="80"><name x="216" y="64">sender_transm</name><label kind="invariant" x="208" y="80">x&lt;= 808</label></location><location id="id7" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="180" y="245">x &lt;= 52</label></location><init ref="id5"/><transition><source ref="id6"/><target ref="id4"/><label kind="guard" x="224" y="0">x&gt;=53</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="synchronisation" x="32" y="-32">begin !</label><label kind="assignment" x="56" y="0">x= 0</label><nail x="80" y="-16"/></transition><transition><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="-108" y="57">cd1 ?</label><label kind="assignment" x="-108" y="72">x= 0</label><nail x="-78" y="42"/><nail x="-18" y="42"/></transition><transition><source ref="id5"/><target ref="id7"/><label kind="synchronisation" x="55" y="140">cd1 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id5"/><target ref="id7"/><label kind="synchronisation" x="55" y="140">busy ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="96" y="80">x == 808</label><label kind="synchronisation" x="64" y="64">end !</label><label kind="assignment" x="55" y="80">x= 0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="312" y="144">x &lt;= 52</label><label kind="synchronisation" x="264" y="144">cd1 ?</label><label kind="assignment" x="130" y="155">x= 0</label><nail x="264" y="152"/></transition><transition><source ref="id7"/><target ref="id6"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="160" y="144">begin !</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id7"/><target ref="id7"/><label kind="guard" x="130" y="200">x &lt;= 52</label><label kind="synchronisation" x="130" y="215">cd1 ?</label><label kind="assignment" x="130" y="230">x= 0</label><nail x="160" y="200"/><nail x="220" y="200"/></transition></template><template><name>P2</name><declaration>clock x;</declaration><location id="id8" x="-80" y="88"><name x="-90" y="58">sender_wait</name></location><location id="id9" x="190" y="80"><name x="180" y="50">sender_transm</name><label kind="invariant" x="180" y="95">x&lt;= 808</label></location><location id="id10" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="208" y="256">x &lt;= 52</label></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="synchronisation" x="64" y="-8">begin !</label><label kind="assignment" x="32" y="-16">x= 0</label><nail x="16" y="0"/></transition><transition><source ref="id8"/><target ref="id8"/><label kind="synchronisation" x="-140" y="73">cd2 ?</label><label kind="assignment" x="-140" y="88">x= 0</label><nail x="-110" y="58"/><nail x="-50" y="58"/></transition><transition><source ref="id8"/><target ref="id10"/><label kind="synchronisation" x="55" y="140">cd2 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id8"/><target ref="id10"/><label kind="synchronisation" x="55" y="140">busy ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id9"/><target ref="id8"/><label kind="guard" x="32" y="96">x == 808</label><label kind="synchronisation" x="8" y="80">end !</label><label kind="assignment" x="80" y="80">x= 0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="130" y="140">cd2 ?</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="130" y="140">begin !</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id10"/><target ref="id10"/><label kind="guard" x="130" y="200">x &lt;= 52</label><label kind="synchronisation" x="130" y="215">cd2 ?</label><label kind="assignment" x="130" y="230">x= 0</label><nail x="160" y="280"/><nail x="200" y="280"/></transition></template><system>system P0, P1, P2;</system></nta>
\ No newline at end of file
E<> ( P1.error and P2.sender_transm)
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// CSMA/CD 9
// Carrier Sense, Multiple-Access with Collision Detection
//
// automatically generated by script genCSMA_CD.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 19 11:48:20 2001
// ------------------------------------------------------------
chan begin, end, busy, cd1, cd2, cd3, cd4, cd5, cd6, cd7, cd8, cd9;</declaration><template><name>P0</name><declaration>clock x;</declaration><location id="id0" x="-120" y="80"><name x="-192" y="48">bus_idle</name></location><location id="id1" x="48" y="80"><name x="24" y="-8">bus_active</name></location><location id="id2" x="208" y="80"><name x="176" y="0">bus_collision1</name><label kind="invariant" x="176" y="24">x &lt;= 26</label></location><location id="id3" x="344" y="80"><name x="334" y="50">bus_collision2</name><label kind="invariant" x="360" y="72">x &lt;= 0</label></location><location id="id4" x="344" y="232"><name x="360" y="216">bus_collision3</name><label kind="invariant" x="352" y="232">x &lt;= 0</label></location><init ref="id0"/><transition><source ref="id4"/><target ref="id0"/><label kind="guard" x="52" y="126">x&lt;=0</label><label kind="synchronisation" x="52" y="141">cd3!</label><label kind="assignment" x="52" y="156">x=0</label><nail x="-120" y="232"/></transition><transition><source ref="id0"/><target ref="id1"/><label kind="synchronisation" x="-72" y="40">begin ?</label><label kind="assignment" x="-72" y="56">x= 0</label></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="120">end ?</label><label kind="assignment" x="-40" y="136">x= 0</label><nail x="48" y="112"/><nail x="-120" y="112"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="guard" x="24" y="-24">x &gt;= 26</label><label kind="synchronisation" x="24" y="8">busy !</label><nail x="16" y="32"/><nail x="80" y="32"/></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="112" y="48">x &lt;= 26</label><label kind="synchronisation" x="112" y="88">begin ?</label><label kind="assignment" x="112" y="104">x= 0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="272" y="25">x &lt;= 26</label><label kind="synchronisation" x="272" y="40">cd1 !</label><label kind="assignment" x="272" y="55">x= 0</label></transition><transition><source ref="id3"/><target ref="id4"/><label kind="guard" x="352" y="152">x &lt;= 0</label><label kind="synchronisation" x="352" y="168">cd2 !</label><label kind="assignment" x="352" y="136">x= 0</label></transition></template><template><name>P1</name><declaration>clock x;</declaration><location id="id5" x="344" y="-24"><name x="334" y="-54">error</name></location><location id="id6" x="-48" y="72"><name x="-120" y="16">sender_wait</name></location><location id="id7" x="192" y="80"><name x="216" y="64">sender_transm</name><label kind="invariant" x="208" y="80">x&lt;= 808</label></location><location id="id8" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="180" y="245">x &lt;= 52</label></location><init ref="id6"/><transition><source ref="id7"/><target ref="id5"/><label kind="guard" x="224" y="0">x&gt;=53</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="synchronisation" x="32" y="-32">begin !</label><label kind="assignment" x="56" y="0">x= 0</label><nail x="80" y="-16"/></transition><transition><source ref="id6"/><target ref="id6"/><label kind="synchronisation" x="-108" y="57">cd1 ?</label><label kind="assignment" x="-108" y="72">x= 0</label><nail x="-78" y="42"/><nail x="-18" y="42"/></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="55" y="140">cd1 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id6"/><target ref="id8"/><label kind="synchronisation" x="55" y="140">busy ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id7"/><target ref="id6"/><label kind="guard" x="96" y="80">x == 808</label><label kind="synchronisation" x="64" y="64">end !</label><label kind="assignment" x="55" y="80">x= 0</label></transition><transition><source ref="id7"/><target ref="id8"/><label kind="guard" x="312" y="144">x &lt;= 52</label><label kind="synchronisation" x="264" y="144">cd1 ?</label><label kind="assignment" x="130" y="155">x= 0</label><nail x="264" y="152"/></transition><transition><source ref="id8"/><target ref="id7"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="160" y="144">begin !</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id8"/><target ref="id8"/><label kind="guard" x="130" y="200">x &lt;= 52</label><label kind="synchronisation" x="130" y="215">cd1 ?</label><label kind="assignment" x="130" y="230">x= 0</label><nail x="160" y="200"/><nail x="220" y="200"/></transition></template><template><name>P2</name><declaration>clock x;</declaration><location id="id9" x="-80" y="88"><name x="-90" y="58">sender_wait</name></location><location id="id10" x="190" y="80"><name x="180" y="50">sender_transm</name><label kind="invariant" x="180" y="95">x&lt;= 808</label></location><location id="id11" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="208" y="256">x &lt;= 52</label></location><init ref="id9"/><transition><source ref="id9"/><target ref="id10"/><label kind="synchronisation" x="64" y="-8">begin !</label><label kind="assignment" x="32" y="-16">x= 0</label><nail x="16" y="0"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="synchronisation" x="-140" y="73">cd2 ?</label><label kind="assignment" x="-140" y="88">x= 0</label><nail x="-110" y="58"/><nail x="-50" y="58"/></transition><transition><source ref="id9"/><target ref="id11"/><label kind="synchronisation" x="55" y="140">cd2 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id9"/><target ref="id11"/><label kind="synchronisation" x="55" y="140">busy ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="32" y="96">x == 808</label><label kind="synchronisation" x="8" y="80">end !</label><label kind="assignment" x="80" y="80">x= 0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="130" y="140">cd2 ?</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id11"/><target ref="id10"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="130" y="140">begin !</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id11"/><target ref="id11"/><label kind="guard" x="130" y="200">x &lt;= 52</label><label kind="synchronisation" x="130" y="215">cd2 ?</label><label kind="assignment" x="130" y="230">x= 0</label><nail x="160" y="280"/><nail x="200" y="280"/></transition></template><template><name>P3</name><declaration>clock x;</declaration><location id="id12" x="40" y="80"><name x="30" y="50">sender_wait</name></location><location id="id13" x="190" y="80"><name x="180" y="50">sender_transm</name><label kind="invariant" x="180" y="95">x&lt;= 808</label></location><location id="id14" x="190" y="230"><name x="180" y="200">sender_retry</name><label kind="invariant" x="180" y="245">x &lt;= 52</label></location><init ref="id12"/><transition><source ref="id12"/><target ref="id13"/><label kind="synchronisation" x="55" y="65">begin !</label><label kind="assignment" x="55" y="80">x= 0</label></transition><transition><source ref="id12"/><target ref="id12"/><label kind="synchronisation" x="-20" y="65">cd3 ?</label><label kind="assignment" x="-20" y="80">x= 0</label><nail x="10" y="50"/><nail x="70" y="50"/></transition><transition><source ref="id12"/><target ref="id14"/><label kind="synchronisation" x="55" y="140">cd3 ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id12"/><target ref="id14"/><label kind="synchronisation" x="55" y="140">busy ?</label><label kind="assignment" x="55" y="155">x= 0</label></transition><transition><source ref="id13"/><target ref="id12"/><label kind="guard" x="55" y="50">x == 808</label><label kind="synchronisation" x="55" y="65">end !</label><label kind="assignment" x="55" y="80">x= 0</label></transition><transition><source ref="id13"/><target ref="id14"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="130" y="140">cd3 ?</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="130" y="125">x &lt;= 52</label><label kind="synchronisation" x="130" y="140">begin !</label><label kind="assignment" x="130" y="155">x= 0</label></transition><transition><source ref="id14"/><target ref="id14"/><label kind="guard" x="130" y="200">x &lt;= 52</label><label kind="synchronisation" x="130" y="215">cd3 ?</label><label kind="assignment" x="130" y="230">x= 0</label><nail x="160" y="200"/><nail x="220" y="200"/></transition></template><system>system P0, P1, P2, P3;</system></nta>
\ No newline at end of file
E<> ( P1.error and P2.sender_transm)
This diff is collapsed.
E<> ( P1.error and P2.sender_transm)
This diff is collapsed.
E<> ( P1.error and P2.sender_transm)
This diff is collapsed.
//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
/*
*/
E<> ( P1.error and P2.sender_transm)
This diff is collapsed.
E<> ( P1.error and P2.sender_transm)
This diff is collapsed.
E<> P1.Error and P2.sender_transm
This diff is collapsed.
//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
/*
*/
E<> P1.Error and P2.sender_transm
This diff is collapsed.
E<> (p2.cs and (p1.cs))
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 9
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2;
int id;
const int k = 2;</declaration><template><name>p1</name><location id="id0" x="40" y="80"><name x="30" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="130" y="125">x1&lt;=k</label><label kind="assignment" x="130" y="155">x1=0,id=1</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="55" y="200">x1&gt;k and id==1</label></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-20" y="155">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="55" y="200">x2&gt;k and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><system>system p1,p2;
</system></nta>
\ No newline at end of file
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 8
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2, x3;
int id;
const int k = 2;
const int kp1 = 3;</declaration><template><name>p1</name><location id="id0" x="32" y="80"><name x="22" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="192" y="104">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="32" y="232"><name x="22" y="202">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="328" y="104">k&gt;=x1</label><label kind="assignment" x="328" y="120">x1=0,id=1</label><nail x="320" y="96"/><nail x="328" y="152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="192" y="128">id==0</label><label kind="assignment" x="192" y="144">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="40" y="248">kp1 &lt;= x1 and id==1</label><nail x="112" y="232"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-48" y="152">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="56" y="240">x2&gt;=kp1 and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><template><name>p3</name><location id="id8" x="40" y="80"><name x="30" y="50">a</name></location><location id="id9" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x3&lt;=k</label></location><location id="id10" x="190" y="230"><name x="180" y="200">c</name></location><location id="id11" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x3=0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x3&lt;=k</label><label kind="assignment" x="130" y="155">x3=0,id=3</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x3=0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="55" y="200">x3&gt;=kp1 and id==3</label></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-20" y="155">x3=0,id=0</label></transition></template><system>system p1, p2, p3;</system></nta>
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 8
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2, x3, x4;
int id;
const int k = 2;
const int kp1 = 3;</declaration><template><name>p1</name><location id="id0" x="32" y="80"><name x="22" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="192" y="104">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="32" y="232"><name x="22" y="202">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="328" y="104">k&gt;=x1</label><label kind="assignment" x="328" y="120">x1=0,id=1</label><nail x="320" y="96"/><nail x="328" y="152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="192" y="128">id==0</label><label kind="assignment" x="192" y="144">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="40" y="248">kp1 &lt;= x1 and id==1</label><nail x="112" y="232"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-48" y="152">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="56" y="240">x2&gt;=kp1 and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><template><name>p3</name><location id="id8" x="40" y="80"><name x="30" y="50">a</name></location><location id="id9" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x3&lt;=k</label></location><location id="id10" x="190" y="230"><name x="180" y="200">c</name></location><location id="id11" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x3=0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x3&lt;=k</label><label kind="assignment" x="130" y="155">x3=0,id=3</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x3=0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="55" y="200">x3&gt;=kp1 and id==3</label></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-20" y="155">x3=0,id=0</label></transition></template><template><name>p4</name><location id="id12" x="40" y="80"><name x="30" y="50">a</name></location><location id="id13" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x4&lt;=k</label></location><location id="id14" x="190" y="230"><name x="180" y="200">c</name></location><location id="id15" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id12"/><transition><source ref="id12"/><target ref="id13"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x4=0</label></transition><transition><source ref="id13"/><target ref="id14"/><label kind="guard" x="130" y="125">x4&lt;=k</label><label kind="assignment" x="130" y="155">x4=0,id=4</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x4=0</label></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="55" y="200">x4&gt;=kp1 and id==4</label></transition><transition><source ref="id15"/><target ref="id12"/><label kind="assignment" x="-20" y="155">x4=0,id=0</label></transition></template><system>system p1, p2, p3, p4;</system></nta>
E<> (p2.cs and (p1.cs))
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 8
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2, x3, x4, x5;
int id;
const int k = 2;
const int kp1 = 3;</declaration><template><name>p1</name><location id="id0" x="32" y="80"><name x="22" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="192" y="104">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="32" y="232"><name x="22" y="202">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="328" y="104">k&gt;=x1</label><label kind="assignment" x="328" y="120">x1=0,id=1</label><nail x="320" y="96"/><nail x="328" y="152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="192" y="128">id==0</label><label kind="assignment" x="192" y="144">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="40" y="248">kp1 &lt;= x1 and id==1</label><nail x="112" y="232"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-48" y="152">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="56" y="240">x2&gt;=kp1 and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><template><name>p3</name><location id="id8" x="40" y="80"><name x="30" y="50">a</name></location><location id="id9" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x3&lt;=k</label></location><location id="id10" x="190" y="230"><name x="180" y="200">c</name></location><location id="id11" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x3=0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x3&lt;=k</label><label kind="assignment" x="130" y="155">x3=0,id=3</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x3=0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="55" y="200">x3&gt;=kp1 and id==3</label></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-20" y="155">x3=0,id=0</label></transition></template><template><name>p4</name><location id="id12" x="40" y="80"><name x="30" y="50">a</name></location><location id="id13" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x4&lt;=k</label></location><location id="id14" x="190" y="230"><name x="180" y="200">c</name></location><location id="id15" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id12"/><transition><source ref="id12"/><target ref="id13"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x4=0</label></transition><transition><source ref="id13"/><target ref="id14"/><label kind="guard" x="130" y="125">x4&lt;=k</label><label kind="assignment" x="130" y="155">x4=0,id=4</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x4=0</label></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="55" y="200">x4&gt;=kp1 and id==4</label></transition><transition><source ref="id15"/><target ref="id12"/><label kind="assignment" x="-20" y="155">x4=0,id=0</label></transition></template><template><name>p5</name><location id="id16" x="40" y="80"><name x="30" y="50">a</name></location><location id="id17" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x5&lt;=k</label></location><location id="id18" x="190" y="230"><name x="180" y="200">c</name></location><location id="id19" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id16"/><transition><source ref="id16"/><target ref="id17"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x5=0</label></transition><transition><source ref="id17"/><target ref="id18"/><label kind="guard" x="130" y="125">x5&lt;=k</label><label kind="assignment" x="130" y="155">x5=0,id=5</label></transition><transition><source ref="id18"/><target ref="id17"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x5=0</label></transition><transition><source ref="id18"/><target ref="id19"/><label kind="guard" x="55" y="200">x5&gt;=kp1 and id==5</label></transition><transition><source ref="id19"/><target ref="id16"/><label kind="assignment" x="-20" y="155">x5=0,id=0</label></transition></template><system>system p1, p2, p3, p4, p5;</system></nta>
E<> (p2.cs and (p1.cs))
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 8
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2, x3, x4, x5, x6;
int id;
const int k = 2;
const int kp1 = 3;</declaration><template><name>p1</name><location id="id0" x="32" y="80"><name x="22" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="192" y="104">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="32" y="232"><name x="22" y="202">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="328" y="104">k&gt;=x1</label><label kind="assignment" x="328" y="120">x1=0,id=1</label><nail x="320" y="96"/><nail x="328" y="152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="192" y="128">id==0</label><label kind="assignment" x="192" y="144">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="40" y="248">kp1 &lt;= x1 and id==1</label><nail x="112" y="232"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-48" y="152">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="56" y="240">x2&gt;=kp1 and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><template><name>p3</name><location id="id8" x="40" y="80"><name x="30" y="50">a</name></location><location id="id9" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x3&lt;=k</label></location><location id="id10" x="190" y="230"><name x="180" y="200">c</name></location><location id="id11" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x3=0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x3&lt;=k</label><label kind="assignment" x="130" y="155">x3=0,id=3</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x3=0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="55" y="200">x3&gt;=kp1 and id==3</label></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-20" y="155">x3=0,id=0</label></transition></template><template><name>p4</name><location id="id12" x="40" y="80"><name x="30" y="50">a</name></location><location id="id13" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x4&lt;=k</label></location><location id="id14" x="190" y="230"><name x="180" y="200">c</name></location><location id="id15" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id12"/><transition><source ref="id12"/><target ref="id13"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x4=0</label></transition><transition><source ref="id13"/><target ref="id14"/><label kind="guard" x="130" y="125">x4&lt;=k</label><label kind="assignment" x="130" y="155">x4=0,id=4</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x4=0</label></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="55" y="200">x4&gt;=kp1 and id==4</label></transition><transition><source ref="id15"/><target ref="id12"/><label kind="assignment" x="-20" y="155">x4=0,id=0</label></transition></template><template><name>p5</name><location id="id16" x="40" y="80"><name x="30" y="50">a</name></location><location id="id17" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x5&lt;=k</label></location><location id="id18" x="190" y="230"><name x="180" y="200">c</name></location><location id="id19" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id16"/><transition><source ref="id16"/><target ref="id17"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x5=0</label></transition><transition><source ref="id17"/><target ref="id18"/><label kind="guard" x="130" y="125">x5&lt;=k</label><label kind="assignment" x="130" y="155">x5=0,id=5</label></transition><transition><source ref="id18"/><target ref="id17"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x5=0</label></transition><transition><source ref="id18"/><target ref="id19"/><label kind="guard" x="55" y="200">x5&gt;=kp1 and id==5</label></transition><transition><source ref="id19"/><target ref="id16"/><label kind="assignment" x="-20" y="155">x5=0,id=0</label></transition></template><template><name>p6</name><location id="id20" x="40" y="80"><name x="30" y="50">a</name></location><location id="id21" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x6&lt;=k</label></location><location id="id22" x="190" y="230"><name x="180" y="200">c</name></location><location id="id23" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id20"/><transition><source ref="id20"/><target ref="id21"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x6=0</label></transition><transition><source ref="id21"/><target ref="id22"/><label kind="guard" x="130" y="125">x6&lt;=k</label><label kind="assignment" x="130" y="155">x6=0,id=6</label></transition><transition><source ref="id22"/><target ref="id21"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x6=0</label></transition><transition><source ref="id22"/><target ref="id23"/><label kind="guard" x="55" y="200">x6&gt;=kp1 and id==6</label></transition><transition><source ref="id23"/><target ref="id20"/><label kind="assignment" x="-20" y="155">x6=0,id=0</label></transition></template><system>system p1, p2, p3, p4, p5, p6;</system></nta>
E<> (p2.cs and (p1.cs))
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 8
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2, x3, x4, x5, x6, x7, x8;
int id;
const int k = 2;
const int kp1 = 3;</declaration><template><name>p1</name><location id="id0" x="32" y="80"><name x="22" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="192" y="104">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="32" y="232"><name x="22" y="202">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="328" y="104">k&gt;=x1</label><label kind="assignment" x="328" y="120">x1=0,id=1</label><nail x="320" y="96"/><nail x="328" y="152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="192" y="128">id==0</label><label kind="assignment" x="192" y="144">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="40" y="248">kp1 &lt;= x1 and id==1</label><nail x="112" y="232"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-48" y="152">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="56" y="240">x2&gt;=kp1 and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><template><name>p3</name><location id="id8" x="40" y="80"><name x="30" y="50">a</name></location><location id="id9" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x3&lt;=k</label></location><location id="id10" x="190" y="230"><name x="180" y="200">c</name></location><location id="id11" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x3=0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x3&lt;=k</label><label kind="assignment" x="130" y="155">x3=0,id=3</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x3=0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="55" y="200">x3&gt;=kp1 and id==3</label></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-20" y="155">x3=0,id=0</label></transition></template><template><name>p4</name><location id="id12" x="40" y="80"><name x="30" y="50">a</name></location><location id="id13" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x4&lt;=k</label></location><location id="id14" x="190" y="230"><name x="180" y="200">c</name></location><location id="id15" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id12"/><transition><source ref="id12"/><target ref="id13"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x4=0</label></transition><transition><source ref="id13"/><target ref="id14"/><label kind="guard" x="130" y="125">x4&lt;=k</label><label kind="assignment" x="130" y="155">x4=0,id=4</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x4=0</label></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="55" y="200">x4&gt;=kp1 and id==4</label></transition><transition><source ref="id15"/><target ref="id12"/><label kind="assignment" x="-20" y="155">x4=0,id=0</label></transition></template><template><name>p5</name><location id="id16" x="40" y="80"><name x="30" y="50">a</name></location><location id="id17" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x5&lt;=k</label></location><location id="id18" x="190" y="230"><name x="180" y="200">c</name></location><location id="id19" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id16"/><transition><source ref="id16"/><target ref="id17"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x5=0</label></transition><transition><source ref="id17"/><target ref="id18"/><label kind="guard" x="130" y="125">x5&lt;=k</label><label kind="assignment" x="130" y="155">x5=0,id=5</label></transition><transition><source ref="id18"/><target ref="id17"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x5=0</label></transition><transition><source ref="id18"/><target ref="id19"/><label kind="guard" x="55" y="200">x5&gt;=kp1 and id==5</label></transition><transition><source ref="id19"/><target ref="id16"/><label kind="assignment" x="-20" y="155">x5=0,id=0</label></transition></template><template><name>p6</name><location id="id20" x="40" y="80"><name x="30" y="50">a</name></location><location id="id21" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x6&lt;=k</label></location><location id="id22" x="190" y="230"><name x="180" y="200">c</name></location><location id="id23" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id20"/><transition><source ref="id20"/><target ref="id21"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x6=0</label></transition><transition><source ref="id21"/><target ref="id22"/><label kind="guard" x="130" y="125">x6&lt;=k</label><label kind="assignment" x="130" y="155">x6=0,id=6</label></transition><transition><source ref="id22"/><target ref="id21"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x6=0</label></transition><transition><source ref="id22"/><target ref="id23"/><label kind="guard" x="55" y="200">x6&gt;=kp1 and id==6</label></transition><transition><source ref="id23"/><target ref="id20"/><label kind="assignment" x="-20" y="155">x6=0,id=0</label></transition></template><template><name>p7</name><location id="id24" x="40" y="80"><name x="30" y="50">a</name></location><location id="id25" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="208" y="72">x7&lt;=k</label></location><location id="id26" x="190" y="230"><name x="180" y="200">c</name></location><location id="id27" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id24"/><transition><source ref="id24"/><target ref="id25"/><label kind="guard" x="88" y="32">id==0</label><label kind="assignment" x="88" y="56">x7=0</label></transition><transition><source ref="id25"/><target ref="id26"/><label kind="guard" x="256" y="128">x7&lt;=k</label><label kind="assignment" x="256" y="152">x7=0,id=7</label><nail x="248" y="144"/></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x7=0</label></transition><transition><source ref="id26"/><target ref="id27"/><label kind="guard" x="48" y="256">x7&gt;=kp1 and id==7</label></transition><transition><source ref="id27"/><target ref="id24"/><label kind="assignment" x="-64" y="152">x7=0,id=0</label></transition></template><system>system p1, p2, p3, p4, p5, p6, p7;</system></nta>
\ No newline at end of file
E<> (p2.cs and (p1.cs))
<?xml version="1.0" encoding="utf-8"?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// ------------------------------------------------------------
// Fischer 8
//
// automatically generated by script generate.awk
// M. Oliver Moeller &lt;omoeller@brics.dk&gt;
// Wed Sep 12 20:44:41 2001
// ------------------------------------------------------------
clock x1, x2, x3, x4, x5, x6, x7, x8;
int id;
const int k = 2;
const int kp1 = 3;</declaration><template><name>p1</name><location id="id0" x="32" y="80"><name x="22" y="50">a</name></location><location id="id1" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x1&lt;=k</label></location><location id="id2" x="190" y="230"><name x="180" y="200">c</name></location><location id="id3" x="32" y="232"><name x="22" y="202">cs</name></location><init ref="id0"/><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x1=0</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="328" y="104">x1&lt;=k</label><label kind="assignment" x="328" y="120">x1=0,id=1</label><nail x="320" y="96"/><nail x="328" y="152"/></transition><transition><source ref="id2"/><target ref="id1"/><label kind="guard" x="192" y="128">id==0</label><label kind="assignment" x="192" y="144">x1=0</label></transition><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="40" y="248">x1&gt;=kp1 and id==1</label><nail x="112" y="232"/></transition><transition><source ref="id3"/><target ref="id0"/><label kind="assignment" x="-20" y="155">x1=0,id=0</label></transition></template><template><name>p2</name><location id="id4" x="40" y="80"><name x="30" y="50">a</name></location><location id="id5" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x2&lt;=k</label></location><location id="id6" x="190" y="230"><name x="180" y="200">c</name></location><location id="id7" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id4"/><transition><source ref="id4"/><target ref="id5"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x2=0</label></transition><transition><source ref="id5"/><target ref="id6"/><label kind="guard" x="130" y="125">x2&lt;=k</label><label kind="assignment" x="130" y="155">x2=0,id=2</label></transition><transition><source ref="id6"/><target ref="id5"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x2=0</label></transition><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="56" y="240">x2&gt;=kp1 and id==2</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="assignment" x="-20" y="155">x2=0,id=0</label></transition></template><template><name>p3</name><location id="id8" x="40" y="80"><name x="30" y="50">a</name></location><location id="id9" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x3&lt;=k</label></location><location id="id10" x="190" y="230"><name x="180" y="200">c</name></location><location id="id11" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id8"/><transition><source ref="id8"/><target ref="id9"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x3=0</label></transition><transition><source ref="id9"/><target ref="id10"/><label kind="guard" x="130" y="125">x3&lt;=k</label><label kind="assignment" x="130" y="155">x3=0,id=3</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x3=0</label></transition><transition><source ref="id10"/><target ref="id11"/><label kind="guard" x="55" y="200">x3&gt;=kp1 and id==3</label></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-20" y="155">x3=0,id=0</label></transition></template><template><name>p4</name><location id="id12" x="40" y="80"><name x="30" y="50">a</name></location><location id="id13" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x4&lt;=k</label></location><location id="id14" x="190" y="230"><name x="180" y="200">c</name></location><location id="id15" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id12"/><transition><source ref="id12"/><target ref="id13"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x4=0</label></transition><transition><source ref="id13"/><target ref="id14"/><label kind="guard" x="130" y="125">x4&lt;=k</label><label kind="assignment" x="130" y="155">x4=0,id=4</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x4=0</label></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="55" y="200">x4&gt;=kp1 and id==4</label></transition><transition><source ref="id15"/><target ref="id12"/><label kind="assignment" x="-20" y="155">x4=0,id=0</label></transition></template><template><name>p5</name><location id="id16" x="40" y="80"><name x="30" y="50">a</name></location><location id="id17" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x5&lt;=k</label></location><location id="id18" x="190" y="230"><name x="180" y="200">c</name></location><location id="id19" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id16"/><transition><source ref="id16"/><target ref="id17"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x5=0</label></transition><transition><source ref="id17"/><target ref="id18"/><label kind="guard" x="130" y="125">x5&lt;=k</label><label kind="assignment" x="130" y="155">x5=0,id=5</label></transition><transition><source ref="id18"/><target ref="id17"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x5=0</label></transition><transition><source ref="id18"/><target ref="id19"/><label kind="guard" x="55" y="200">x5&gt;=kp1 and id==5</label></transition><transition><source ref="id19"/><target ref="id16"/><label kind="assignment" x="-20" y="155">x5=0,id=0</label></transition></template><template><name>p6</name><location id="id20" x="40" y="80"><name x="30" y="50">a</name></location><location id="id21" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x6&lt;=k</label></location><location id="id22" x="190" y="230"><name x="180" y="200">c</name></location><location id="id23" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id20"/><transition><source ref="id20"/><target ref="id21"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x6=0</label></transition><transition><source ref="id21"/><target ref="id22"/><label kind="guard" x="130" y="125">x6&lt;=k</label><label kind="assignment" x="130" y="155">x6=0,id=6</label></transition><transition><source ref="id22"/><target ref="id21"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x6=0</label></transition><transition><source ref="id22"/><target ref="id23"/><label kind="guard" x="55" y="200">x6&gt;=kp1 and id==6</label></transition><transition><source ref="id23"/><target ref="id20"/><label kind="assignment" x="-20" y="155">x6=0,id=0</label></transition></template><template><name>p7</name><location id="id24" x="40" y="80"><name x="30" y="50">a</name></location><location id="id25" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x7&lt;=k</label></location><location id="id26" x="190" y="230"><name x="180" y="200">c</name></location><location id="id27" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id24"/><transition><source ref="id24"/><target ref="id25"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x7=0</label></transition><transition><source ref="id25"/><target ref="id26"/><label kind="guard" x="130" y="125">x7&lt;=k</label><label kind="assignment" x="130" y="155">x7=0,id=7</label></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x7=0</label></transition><transition><source ref="id26"/><target ref="id27"/><label kind="guard" x="55" y="200">x7&gt;=kp1 and id==7</label></transition><transition><source ref="id27"/><target ref="id24"/><label kind="assignment" x="-20" y="155">x7=0,id=0</label></transition></template><template><name>p8</name><location id="id28" x="40" y="80"><name x="30" y="50">a</name></location><location id="id29" x="190" y="80"><name x="180" y="50">b</name><label kind="invariant" x="180" y="95">x8&lt;=k</label></location><location id="id30" x="190" y="230"><name x="180" y="200">c</name></location><location id="id31" x="40" y="230"><name x="30" y="200">cs</name></location><init ref="id28"/><transition><source ref="id28"/><target ref="id29"/><label kind="guard" x="55" y="50">id==0</label><label kind="assignment" x="55" y="80">x8=0</label></transition><transition><source ref="id29"/><target ref="id30"/><label kind="guard" x="130" y="125">x8&lt;=k</label><label kind="assignment" x="130" y="155">x8=0,id=8</label></transition><transition><source ref="id30"/><target ref="id29"/><label kind="guard" x="130" y="125">id==0</label><label kind="assignment" x="130" y="155">x8=0</label></transition><transition><source ref="id30"/><target ref="id31"/><label kind="guard" x="55" y="200">x8&gt;=kp1 and id==8</label></transition><transition><source ref="id31"/><target ref="id28"/><label kind="assignment" x="-20" y="155">x8=0,id=0</label></transition></template><system>system p1, p2, p3, p4, p5, p6, p7, p8;</system></nta>
\ No newline at end of file
E<> (p2.cs and (p1.cs))
This diff is collapsed.
//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
/*
*/
E<>(p2.cs and p1.cs)
This diff is collapsed.
E<> ST1.station_z_async and ST2.station_z_async
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment