// Testfile dumped by Ultimate at 2011/12/17 15:44:51 BranchingProcess bp = finitePrefix(net); print(numberOfConditions(bp)); assert(numberOfConditions(bp) == 230); assert(isEmpty(net)); PetriNet net = ( alphabet = {"A" "B" "C" "D" "E" "F" "G" "H" "I" "J" "K" "L" "M" "N" "O" "P" "Q" "R" "S" "T" "U" "V" "W" "X" }, places = {"Place01" "Place02" "Place03" "Place04" "Place05" "Place06" "Place07" "Place08" "Place09" "Place10" "Place11" "Place12" "Place13" "Place14" "Place15" "Place16" "Place17" "Place18" "Place19" "Place20" "Place21" "Place22" "Place23" "Place24" "Place25" "Place26" "Place27" "Place28" "Place29" "Place30" "Place31" "Place32" "Place33" "Place34" "Place35" "Place36" "Place37" "Place38" "Place39" "Place40" "Place41" "Place42" "Place43" "Place44" "Place45" "Place46" "Place47" "Place48" "Place49" "Place50" }, transitions = { ( {"Place06" "Place02" "Place26" "Place47" "Place45" } "P" {"Place36" "Place04" "Place05" "Place49" "Place50" } ) ( {"Place23" "Place30" "Place15" "Place26" } "K" {"Place29" "Place30" "Place04" "Place14" } ) ( {"Place32" "Place17" "Place16" "Place38" "Place15" "Place26" } "M" {"Place37" "Place01" "Place41" "Place30" "Place04" "Place14" } ) ( {"Place23" "Place30" "Place24" "Place14" } "K" {"Place29" "Place30" "Place24" "Place14" } ) ( {"Place28" } "F" {"Place06" } ) ( {"Place40" "Place30" "Place24" "Place14" } "Q" {"Place35" "Place30" "Place24" "Place14" } ) ( {"Place42" "Place16" "Place38" "Place24" "Place14" } "N" {"Place18" "Place41" "Place30" "Place24" "Place14" } ) ( {"Place36" "Place20" "Place03" "Place14" "Place46" } "I" {"Place31" "Place22" "Place21" "Place14" "Place46" } ) ( {"Place31" "Place03" } "J" {"Place34" "Place03" } ) ( {"Place32" "Place17" "Place16" "Place38" "Place24" "Place14" } "M" {"Place37" "Place01" "Place41" "Place30" "Place24" "Place14" } ) ( {"Place48" "Place27" } "L" {"Place33" "Place27" } ) ( {"Place10" "Place41" "Place30" "Place04" "Place24" } "B" {"Place23" "Place16" "Place38" "Place25" "Place26" } ) ( {"Place23" "Place16" "Place38" "Place25" "Place26" } "K" {"Place29" "Place41" "Place30" "Place04" "Place24" } ) ( {"Place29" "Place04" "Place05" "Place49" "Place50" } "O" {"Place28" "Place02" "Place26" "Place47" "Place45" } ) ( {"Place33" "Place22" "Place21" "Place25" "Place14" "Place49" "Place46" } "R" {"Place12" "Place20" "Place03" "Place15" "Place24" "Place44" "Place45" } ) ( {"Place29" "Place04" "Place05" "Place45" "Place46" } "O" {"Place28" "Place02" "Place26" "Place45" "Place46" } ) ( {"Place33" "Place22" "Place21" "Place24" "Place49" "Place46" } "R" {"Place12" "Place20" "Place03" "Place24" "Place44" "Place45" } ) ( {"Place29" "Place25" "Place05" "Place44" "Place50" } "O" {"Place28" "Place02" "Place24" "Place47" "Place46" } ) ( {"Place37" "Place01" } "H" {"Place43" "Place28" } ) ( {"Place23" "Place30" "Place25" "Place26" } "K" {"Place29" "Place30" "Place04" "Place24" } ) ( {"Place35" "Place22" "Place27" } "G" {"Place43" "Place09" "Place03" } ) ( {"Place06" "Place02" "Place26" "Place50" } "P" {"Place36" "Place04" "Place05" "Place50" } ) ( {"Place29" "Place04" "Place05" "Place44" "Place50" } "O" {"Place28" "Place02" "Place26" "Place47" "Place46" } ) ( {"Place36" "Place21" "Place15" "Place24" "Place44" "Place45" } "I" {"Place31" "Place21" "Place25" "Place14" "Place49" "Place46" } ) ( {"Place33" "Place22" "Place21" "Place24" "Place45" } "R" {"Place12" "Place20" "Place03" "Place24" "Place45" } ) ( {"Place33" "Place22" "Place21" "Place25" "Place14" "Place45" } "R" {"Place12" "Place20" "Place03" "Place15" "Place24" "Place45" } ) ( {"Place23" "Place16" "Place38" "Place15" "Place26" } "K" {"Place29" "Place41" "Place30" "Place04" "Place14" } ) ( {"Place43" } "X" {"Place48" } ) ( {"Place40" "Place30" "Place25" "Place26" } "Q" {"Place35" "Place30" "Place04" "Place24" } ) ( {"Place34" "Place38" } "A" {"Place11" "Place38" } ) ( {"Place10" "Place41" "Place30" "Place26" } "B" {"Place23" "Place16" "Place38" "Place26" } ) ( {"Place29" "Place15" "Place05" "Place45" "Place46" } "O" {"Place28" "Place02" "Place14" "Place45" "Place46" } ) ( {"Place28" "Place38" "Place30" "Place21" "Place03" "Place27" "Place26" "Place24" "Place05" "Place14" "Place45" "Place46" "Place50" } "D" {"Place07" "Place38" "Place30" "Place21" "Place03" "Place27" "Place26" "Place24" "Place05" "Place14" "Place45" "Place46" "Place50" } ) ( {"Place23" "Place16" "Place38" "Place24" "Place14" } "K" {"Place29" "Place41" "Place30" "Place24" "Place14" } ) ( {"Place33" "Place03" "Place24" "Place49" "Place46" } "R" {"Place12" "Place03" "Place24" "Place44" "Place45" } ) ( {"Place34" "Place30" "Place24" "Place14" } "E" {"Place10" "Place30" "Place24" "Place14" } ) ( {"Place40" "Place16" "Place38" "Place24" "Place14" } "Q" {"Place35" "Place41" "Place30" "Place24" "Place14" } ) ( {"Place34" "Place16" "Place38" "Place24" "Place14" } "E" {"Place10" "Place41" "Place30" "Place24" "Place14" } ) ( {"Place32" "Place17" "Place16" "Place38" "Place25" "Place26" } "M" {"Place37" "Place01" "Place41" "Place30" "Place04" "Place24" } ) ( {"Place35" "Place21" "Place03" } "G" {"Place43" "Place21" "Place03" } ) ( {"Place18" "Place38" "Place04" "Place24" } "S" {"Place40" "Place38" "Place25" "Place26" } ) ( {"Place29" "Place15" "Place05" "Place44" "Place50" } "O" {"Place28" "Place02" "Place14" "Place47" "Place46" } ) ( {"Place18" "Place38" "Place26" } "S" {"Place40" "Place38" "Place26" } ) ( {"Place32" "Place17" "Place30" "Place15" "Place26" } "M" {"Place37" "Place01" "Place30" "Place04" "Place14" } ) ( {"Place33" "Place03" "Place24" "Place45" } "R" {"Place12" "Place03" "Place24" "Place45" } ) ( {"Place36" "Place20" "Place03" "Place15" "Place24" "Place46" } "I" {"Place31" "Place22" "Place21" "Place25" "Place14" "Place46" } ) ( {"Place13" } "V" {"Place19" } ) ( {"Place36" "Place20" "Place03" "Place15" "Place24" "Place44" "Place45" } "I" {"Place31" "Place22" "Place21" "Place25" "Place14" "Place49" "Place46" } ) ( {"Place29" "Place26" "Place24" "Place14" "Place45" "Place46" } "O" {"Place28" "Place26" "Place24" "Place14" "Place45" "Place46" } ) ( {"Place48" "Place09" "Place21" } "L" {"Place33" "Place20" "Place27" } ) ( {"Place43" "Place38" "Place30" "Place21" "Place03" "Place27" "Place26" "Place24" "Place05" "Place14" "Place45" "Place46" "Place50" } "T" {"Place13" "Place38" "Place30" "Place21" "Place03" "Place27" "Place26" "Place24" "Place05" "Place14" "Place45" "Place46" "Place50" } ) ( {"Place33" "Place03" "Place25" "Place14" "Place49" "Place46" } "R" {"Place12" "Place03" "Place15" "Place24" "Place44" "Place45" } ) ( {"Place29" "Place26" "Place24" "Place14" "Place49" "Place50" } "O" {"Place28" "Place26" "Place24" "Place14" "Place47" "Place45" } ) ( {"Place42" "Place30" "Place24" "Place14" } "N" {"Place18" "Place30" "Place24" "Place14" } ) ( {"Place40" "Place30" "Place15" "Place26" } "Q" {"Place35" "Place30" "Place04" "Place14" } ) ( {"Place12" "Place14" "Place46" } "U" {"Place42" "Place14" "Place46" } ) ( {"Place06" "Place05" "Place50" } "P" {"Place36" "Place05" "Place50" } ) ( {"Place29" "Place26" "Place24" "Place14" "Place44" "Place50" } "O" {"Place28" "Place26" "Place24" "Place14" "Place47" "Place46" } ) ( {"Place32" "Place17" "Place30" "Place24" "Place14" } "M" {"Place37" "Place01" "Place30" "Place24" "Place14" } ) ( {"Place07" } "W" {"Place08" } ) ( {"Place29" "Place25" "Place05" "Place45" "Place46" } "O" {"Place28" "Place02" "Place24" "Place45" "Place46" } ) ( {"Place06" "Place05" "Place47" "Place45" } "P" {"Place36" "Place05" "Place49" "Place50" } ) ( {"Place29" "Place15" "Place05" "Place49" "Place50" } "O" {"Place28" "Place02" "Place14" "Place47" "Place45" } ) ( {"Place35" "Place20" "Place27" } "G" {"Place43" "Place09" "Place21" } ) ( {"Place33" "Place03" "Place25" "Place14" "Place45" } "R" {"Place12" "Place03" "Place15" "Place24" "Place45" } ) ( {"Place40" "Place16" "Place38" "Place15" "Place26" } "Q" {"Place35" "Place41" "Place30" "Place04" "Place14" } ) ( {"Place18" "Place41" "Place30" "Place04" "Place24" } "S" {"Place40" "Place16" "Place38" "Place25" "Place26" } ) ( {"Place10" "Place38" "Place26" } "B" {"Place23" "Place38" "Place26" } ) ( {"Place40" "Place16" "Place38" "Place25" "Place26" } "Q" {"Place35" "Place41" "Place30" "Place04" "Place24" } ) ( {"Place10" "Place38" "Place04" "Place24" } "B" {"Place23" "Place38" "Place25" "Place26" } ) ( {"Place36" "Place20" "Place03" "Place14" "Place44" "Place45" } "I" {"Place31" "Place22" "Place21" "Place14" "Place49" "Place46" } ) ( {"Place36" "Place21" "Place14" "Place44" "Place45" } "I" {"Place31" "Place21" "Place14" "Place49" "Place46" } ) ( {"Place29" "Place25" "Place05" "Place49" "Place50" } "O" {"Place28" "Place02" "Place24" "Place47" "Place45" } ) ( {"Place36" "Place21" "Place15" "Place24" "Place46" } "I" {"Place31" "Place21" "Place25" "Place14" "Place46" } ) ( {"Place32" "Place17" "Place30" "Place25" "Place26" } "M" {"Place37" "Place01" "Place30" "Place04" "Place24" } ) ( {"Place42" "Place38" } "C" {"Place39" "Place38" } ) ( {"Place18" "Place41" "Place30" "Place26" } "S" {"Place40" "Place16" "Place38" "Place26" } ) ( {"Place36" "Place21" "Place14" "Place46" } "I" {"Place31" "Place21" "Place14" "Place46" } ) }, initialMarking = {"Place14" "Place16" "Place17" "Place21" "Place45" "Place46" "Place24" "Place47" "Place26" "Place02" "Place03" "Place32" "Place38" "Place09" }, acceptingPlaces = {"Place39" "Place11" } );