// Benchmark for difference of Petri net and DFA // Generated from // Bakery.bpl_AllErrorsAtOnce_Iteration7_AbstractionAfterDifference.ats (2018/08/13 05:05:19) // Bakery.bpl_AllErrorsAtOnce_Iteration8_EagerFloydHoareAutomaton.ats (2018/08/13 05:05:19) PetriNet net = ( alphabet = {"assume true;" "n1 := n0 + 1;" "assume n0 == 0 || n1 < n0;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n1 := 0;" "assume !true;" "assume true;" "assume true;" "n0 := n1 + 1;" "assume n1 == 0 || n0 < n1;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n0 := 0;" "assume !true;" "assume true;" "critical := 0;n0 := 0;n1 := 1;assume true;" }, places = {"131#(and (<= 2 n0) (<= 1 n1))" "5#L56true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "7#L57true" "135#true" "137#(<= 0 n1)" "9#L58true" "10#L54true" "139#(<= 2 n1)" "12#L59true" "13#L60true" "14#L55true" "15#~initENTRYtrue" "17#L38true" "18#L39true" "20#L35true" "21#L40true" "22#L41true" "24#L36true" "25#L37true" "26#Thread0Err0ASSERT_VIOLATIONASSERTtrue" "27#~initENTRYtrue" "28#true" "30#(= critical 0)" "Black: 28#true" "Black: 30#(= critical 0)" "34#true" "36#(<= 1 n1)" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "41#true" "43#(= n0 0)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "45#(<= 1 n1)" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "52#(<= 1 n1)" "53#(<= 2 n0)" "54#(and (<= 2 n0) (<= (+ n0 1) n1))" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 52#(<= 1 n1)" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "61#true" "63#(<= 0 n1)" "65#(and (<= 1 n0) (<= (+ n0 1) n1))" "67#(and (<= 0 n1) (<= 1 n0))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 61#true" "Black: 63#(<= 0 n1)" "74#true" "76#(= n0 0)" "77#(and (= n0 0) (<= (+ n0 1) n1))" "79#(<= 2 n0)" "80#(and (<= 2 n0) (<= (+ n0 1) n1))" "213#(and (<= 0 n1) (not (= n1 0)))" "216#(and (<= 0 n1) (not (= n1 0)) (<= (+ n1 1) n0))" "219#(and (<= 2 n1) (<= 1 n0))" "222#(and (<= 0 n1) (<= 1 n0))" "Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "Black: 222#(and (<= 0 n1) (<= 1 n0))" }, transitions = { ({"5#L56true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" } "assume n0 == 0 || n1 < n0;" {"Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "7#L57true" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" }) ({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "52#(<= 1 n1)" "36#(<= 1 n1)" "213#(and (<= 0 n1) (not (= n1 0)))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "24#L36true" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "63#(<= 0 n1)" } "n0 := n1 + 1;" {"131#(and (<= 2 n0) (<= 1 n1))" "67#(and (<= 0 n1) (<= 1 n0))" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "216#(and (<= 0 n1) (not (= n1 0)) (<= (+ n1 1) n0))" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 63#(<= 0 n1)" "25#L37true" "Black: 52#(<= 1 n1)" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" }) ({"Black: 30#(= critical 0)" "7#L57true" "28#true" } "assume critical == 0;" {"Black: 28#true" "9#L58true" "30#(= critical 0)" }) ({"Black: 30#(= critical 0)" "34#true" "135#true" "Black: 36#(<= 1 n1)" "Black: 63#(<= 0 n1)" "41#true" "74#true" "15#~initENTRYtrue" "50#true" "Black: 52#(<= 1 n1)" "27#~initENTRYtrue" "28#true" "61#true" } "critical := 0;n0 := 0;n1 := 1;assume true;" {"Black: 28#true" "52#(<= 1 n1)" "36#(<= 1 n1)" "20#L35true" "213#(and (<= 0 n1) (not (= n1 0)))" "Black: 61#true" "10#L54true" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "30#(= critical 0)" "63#(<= 0 n1)" }) ({"50#true" "34#true" "131#(and (<= 2 n0) (<= 1 n1))" "135#true" "Black: 63#(<= 0 n1)" "61#true" "13#L60true" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" } "n1 := 0;" {"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "34#true" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 61#true" "137#(<= 0 n1)" "41#true" "10#L54true" "79#(<= 2 n0)" "63#(<= 0 n1)" }) ({"Black: 43#(= n0 0)" "50#true" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "22#L41true" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "41#true" "79#(<= 2 n0)" } "n0 := 0;" {"50#true" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "20#L35true" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "43#(= n0 0)" "76#(= n0 0)" }) ({"Black: 43#(= n0 0)" "50#true" "34#true" "135#true" "Black: 63#(<= 0 n1)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "61#true" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 61#true" "137#(<= 0 n1)" "10#L54true" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" }) ({"Black: 28#true" "18#L39true" "30#(= critical 0)" } "critical := 1;" {"Black: 30#(= critical 0)" "21#L40true" "28#true" }) ({"50#true" "34#true" "135#true" "Black: 63#(<= 0 n1)" "43#(= n0 0)" "77#(and (= n0 0) (<= (+ n0 1) n1))" "61#true" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 61#true" "137#(<= 0 n1)" "10#L54true" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" }) ({"Black: 219#(and (<= 2 n1) (<= 1 n0))" "131#(and (<= 2 n0) (<= 1 n1))" "67#(and (<= 0 n1) (<= 1 n0))" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 36#(<= 1 n1)" "216#(and (<= 0 n1) (not (= n1 0)) (<= (+ n1 1) n0))" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" "14#L55true" } "n1 := n0 + 1;" {"65#(and (<= 1 n0) (<= (+ n0 1) n1))" "36#(<= 1 n1)" "5#L56true" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "45#(<= 1 n1)" "80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "54#(and (<= 2 n0) (<= (+ n0 1) n1))" "219#(and (<= 2 n1) (<= 1 n0))" "Black: 56#(and (<= 2 n0) (<= 1 n1))" }) ({"Black: 28#true" "12#L59true" } "critical := 0;" {"Black: 28#true" "13#L60true" }) ({"50#true" "34#true" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 61#true" "41#true" "74#true" "13#L60true" } "n1 := 0;" {"Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "50#true" "34#true" "Black: 61#true" "41#true" "74#true" "10#L54true" "222#(and (<= 0 n1) (<= 1 n0))" }) ({"34#true" "52#(<= 1 n1)" "Black: 61#true" "139#(<= 2 n1)" "43#(= n0 0)" "77#(and (= n0 0) (<= (+ n0 1) n1))" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 61#true" "137#(<= 0 n1)" "Black: 52#(<= 1 n1)" "10#L54true" "43#(= n0 0)" "76#(= n0 0)" }) ({"Black: 28#true" "17#L38true" } "assume critical == 0;" {"Black: 28#true" "18#L39true" }) ({"Black: 43#(= n0 0)" "65#(and (<= 1 n0) (<= (+ n0 1) n1))" "50#true" "22#L41true" "Black: 63#(<= 0 n1)" "41#true" "74#true" "219#(and (<= 2 n1) (<= 1 n0))" } "n0 := 0;" {"Black: 219#(and (<= 2 n1) (<= 1 n0))" "50#true" "20#L35true" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "139#(<= 2 n1)" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" }) ({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "25#L37true" "Black: 56#(and (<= 2 n0) (<= 1 n1))" } "assume n1 == 0 || n0 < n1;" {"17#L38true" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 56#(and (<= 2 n0) (<= 1 n1))" }) ({"Black: 222#(and (<= 0 n1) (<= 1 n0))" "131#(and (<= 2 n0) (<= 1 n1))" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 61#true" "13#L60true" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" } "n1 := 0;" {"Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "34#true" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 61#true" "41#true" "10#L54true" "79#(<= 2 n0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "53#(<= 2 n0)" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "222#(and (<= 0 n1) (<= 1 n0))" }) ({"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "34#true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 61#true" "137#(<= 0 n1)" "14#L55true" "79#(<= 2 n0)" "63#(<= 0 n1)" } "n1 := n0 + 1;" {"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "34#true" "5#L56true" "135#true" "Black: 63#(<= 0 n1)" "61#true" }) ({"Black: 30#(= critical 0)" "7#L57true" } "assume !(critical == 0);" {"Black: 30#(= critical 0)" "6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" }) ({"Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "36#(<= 1 n1)" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "139#(<= 2 n1)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "52#(<= 1 n1)" "24#L36true" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "63#(<= 0 n1)" } "n0 := n1 + 1;" {"131#(and (<= 2 n0) (<= 1 n1))" "67#(and (<= 0 n1) (<= 1 n0))" "37#(and (<= 1 n1) (<= (+ n1 1) n0))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 63#(<= 0 n1)" "25#L37true" "Black: 52#(<= 1 n1)" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" }) ({"Black: 28#true" "7#L57true" } "assume critical == 0;" {"Black: 28#true" "9#L58true" }) ({"Black: 28#true" "9#L58true" "30#(= critical 0)" } "critical := 1;" {"Black: 30#(= critical 0)" "28#true" "12#L59true" }) ({"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "65#(and (<= 1 n0) (<= (+ n0 1) n1))" "54#(and (<= 2 n0) (<= (+ n0 1) n1))" "22#L41true" "Black: 63#(<= 0 n1)" "Black: 52#(<= 1 n1)" "219#(and (<= 2 n1) (<= 1 n0))" "45#(<= 1 n1)" } "n0 := 0;" {"Black: 219#(and (<= 2 n1) (<= 1 n0))" "52#(<= 1 n1)" "20#L35true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "139#(<= 2 n1)" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "63#(<= 0 n1)" }) ({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "135#true" "Black: 36#(<= 1 n1)" "24#L36true" "Black: 63#(<= 0 n1)" "Black: 52#(<= 1 n1)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" } "n0 := n1 + 1;" {"131#(and (<= 2 n0) (<= 1 n1))" "135#true" "Black: 36#(<= 1 n1)" "25#L37true" "Black: 63#(<= 0 n1)" "Black: 52#(<= 1 n1)" "46#(and (<= 1 n1) (<= (+ n1 1) n0))" }) ({"Black: 30#(= critical 0)" "21#L40true" "28#true" } "critical := 0;" {"Black: 28#true" "22#L41true" "30#(= critical 0)" }) ({"Black: 43#(= n0 0)" "52#(<= 1 n1)" "36#(<= 1 n1)" "Black: 61#true" "139#(<= 2 n1)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 36#(<= 1 n1)" "Black: 61#true" "137#(<= 0 n1)" "Black: 52#(<= 1 n1)" "10#L54true" "43#(= n0 0)" "76#(= n0 0)" }) ({"Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 36#(<= 1 n1)" "24#L36true" "Black: 52#(<= 1 n1)" "139#(<= 2 n1)" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" } "n0 := n1 + 1;" {"Black: 43#(= n0 0)" "67#(and (<= 0 n1) (<= 1 n0))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "Black: 63#(<= 0 n1)" "41#true" "25#L37true" "74#true" "Black: 52#(<= 1 n1)" }) ({"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 43#(= n0 0)" "50#true" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "22#L41true" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "41#true" } "n0 := 0;" {"50#true" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "20#L35true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "43#(= n0 0)" "77#(and (= n0 0) (<= (+ n0 1) n1))" }) ({"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "50#true" "34#true" "135#true" "Black: 63#(<= 0 n1)" "41#true" "61#true" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 61#true" "137#(<= 0 n1)" "41#true" "10#L54true" "79#(<= 2 n0)" "63#(<= 0 n1)" }) ({"Black: 43#(= n0 0)" "67#(and (<= 0 n1) (<= 1 n0))" "53#(<= 2 n0)" "22#L41true" "Black: 63#(<= 0 n1)" "41#true" "222#(and (<= 0 n1) (<= 1 n0))" "79#(<= 2 n0)" } "n0 := 0;" {"50#true" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "20#L35true" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "137#(<= 0 n1)" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" }) ({"50#true" "34#true" "Black: 61#true" "137#(<= 0 n1)" "43#(= n0 0)" "76#(= n0 0)" "14#L55true" "63#(<= 0 n1)" } "n1 := n0 + 1;" {"Black: 43#(= n0 0)" "50#true" "34#true" "5#L56true" "135#true" "Black: 63#(<= 0 n1)" "44#(and (= n0 0) (<= (+ n0 1) n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "61#true" }) ({"34#true" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "131#(and (<= 2 n0) (<= 1 n1))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 61#true" "41#true" "13#L60true" } "n1 := 0;" {"Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "34#true" "53#(<= 2 n0)" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 61#true" "41#true" "10#L54true" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "222#(and (<= 0 n1) (<= 1 n0))" "79#(<= 2 n0)" }) ({"Black: 30#(= critical 0)" "18#L39true" } "critical := 1;" {"Black: 30#(= critical 0)" "21#L40true" }) ({"50#true" "34#true" "Black: 61#true" "139#(<= 2 n1)" "43#(= n0 0)" "76#(= n0 0)" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 61#true" "137#(<= 0 n1)" "10#L54true" "43#(= n0 0)" "76#(= n0 0)" }) ({"Black: 131#(and (<= 2 n0) (<= 1 n1))" "135#true" "Black: 36#(<= 1 n1)" "24#L36true" "Black: 63#(<= 0 n1)" "Black: 52#(<= 1 n1)" "43#(= n0 0)" "77#(and (= n0 0) (<= (+ n0 1) n1))" } "n0 := n1 + 1;" {"Black: 43#(= n0 0)" "131#(and (<= 2 n0) (<= 1 n1))" "135#true" "Black: 36#(<= 1 n1)" "41#true" "25#L37true" "Black: 63#(<= 0 n1)" "Black: 52#(<= 1 n1)" }) ({"20#L35true" } "assume true;" {"24#L36true" }) ({"Black: 30#(= critical 0)" "28#true" "12#L59true" } "critical := 0;" {"Black: 28#true" "13#L60true" "30#(= critical 0)" }) ({"Black: 222#(and (<= 0 n1) (<= 1 n0))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 36#(<= 1 n1)" "24#L36true" "137#(<= 0 n1)" "Black: 52#(<= 1 n1)" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" } "n0 := n1 + 1;" {"Black: 43#(= n0 0)" "67#(and (<= 0 n1) (<= 1 n0))" "Black: 36#(<= 1 n1)" "Black: 63#(<= 0 n1)" "41#true" "25#L37true" "74#true" "Black: 52#(<= 1 n1)" "222#(and (<= 0 n1) (<= 1 n0))" }) ({"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "34#true" "67#(and (<= 0 n1) (<= 1 n0))" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "53#(<= 2 n0)" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" "222#(and (<= 0 n1) (<= 1 n0))" "14#L55true" "79#(<= 2 n0)" } "n1 := n0 + 1;" {"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 43#(= n0 0)" "65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "34#true" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "5#L56true" "54#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "219#(and (<= 2 n1) (<= 1 n0))" }) ({"Black: 43#(= n0 0)" "50#true" "67#(and (<= 0 n1) (<= 1 n0))" "22#L41true" "Black: 63#(<= 0 n1)" "41#true" "74#true" "222#(and (<= 0 n1) (<= 1 n0))" } "n0 := 0;" {"50#true" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "20#L35true" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "137#(<= 0 n1)" "43#(= n0 0)" "76#(= n0 0)" "63#(<= 0 n1)" }) ({"17#L38true" "Black: 30#(= critical 0)" } "assume !(critical == 0);" {"Black: 30#(= critical 0)" "26#Thread0Err0ASSERT_VIOLATIONASSERTtrue" }) ({"Black: 30#(= critical 0)" "17#L38true" "28#true" } "assume critical == 0;" {"Black: 28#true" "18#L39true" "30#(= critical 0)" }) ({"50#true" "34#true" "131#(and (<= 2 n0) (<= 1 n1))" "135#true" "Black: 63#(<= 0 n1)" "41#true" "61#true" "13#L60true" } "n1 := 0;" {"50#true" "34#true" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 61#true" "137#(<= 0 n1)" "41#true" "10#L54true" "79#(<= 2 n0)" "63#(<= 0 n1)" }) ({"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 43#(= n0 0)" "65#(and (<= 1 n0) (<= (+ n0 1) n1))" "54#(and (<= 2 n0) (<= (+ n0 1) n1))" "22#L41true" "Black: 63#(<= 0 n1)" "41#true" "Black: 52#(<= 1 n1)" "219#(and (<= 2 n1) (<= 1 n0))" } "n0 := 0;" {"Black: 219#(and (<= 2 n1) (<= 1 n0))" "52#(<= 1 n1)" "20#L35true" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "139#(<= 2 n1)" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" "43#(= n0 0)" "77#(and (= n0 0) (<= (+ n0 1) n1))" "63#(<= 0 n1)" }) ({"Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "131#(and (<= 2 n0) (<= 1 n1))" "Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "25#L37true" "Black: 56#(and (<= 2 n0) (<= 1 n1))" } "assume n1 == 0 || n0 < n1;" {"80#(and (<= 2 n0) (<= (+ n0 1) n1))" "17#L38true" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 56#(and (<= 2 n0) (<= 1 n1))" }) ({"Black: 28#true" "21#L40true" } "critical := 0;" {"Black: 28#true" "22#L41true" }) ({"10#L54true" } "assume true;" {"14#L55true" }) ({"Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "52#(<= 1 n1)" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 36#(<= 1 n1)" "24#L36true" "139#(<= 2 n1)" "43#(= n0 0)" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "77#(and (= n0 0) (<= (+ n0 1) n1))" "63#(<= 0 n1)" } "n0 := n1 + 1;" {"Black: 43#(= n0 0)" "131#(and (<= 2 n0) (<= 1 n1))" "67#(and (<= 0 n1) (<= 1 n0))" "199#(and (<= 2 n1) (<= (+ n1 1) n0))" "Black: 36#(<= 1 n1)" "56#(and (<= 2 n0) (<= 1 n1))" "Black: 63#(<= 0 n1)" "41#true" "25#L37true" "Black: 52#(<= 1 n1)" }) ({"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "52#(<= 1 n1)" "36#(<= 1 n1)" "213#(and (<= 0 n1) (not (= n1 0)))" "Black: 61#true" "77#(and (= n0 0) (<= (+ n0 1) n1))" "14#L55true" "63#(<= 0 n1)" } "n1 := n0 + 1;" {"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "34#true" "5#L56true" "135#true" "Black: 36#(<= 1 n1)" "Black: 63#(<= 0 n1)" "Black: 52#(<= 1 n1)" "77#(and (= n0 0) (<= (+ n0 1) n1))" "61#true" }) ({"Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "50#true" "34#true" "67#(and (<= 0 n1) (<= 1 n0))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "74#true" "222#(and (<= 0 n1) (<= 1 n0))" "14#L55true" } "n1 := n0 + 1;" {"Black: 43#(= n0 0)" "65#(and (<= 1 n0) (<= (+ n0 1) n1))" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "34#true" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "5#L56true" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "74#true" "219#(and (<= 2 n1) (<= 1 n0))" }) ({"Black: 30#(= critical 0)" "9#L58true" } "critical := 1;" {"Black: 30#(= critical 0)" "12#L59true" }) }, initialMarking = {"Black: 80#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 131#(and (<= 2 n0) (<= 1 n1))" "Black: 65#(and (<= 1 n0) (<= (+ n0 1) n1))" "135#true" "Black: 67#(and (<= 0 n1) (<= 1 n0))" "Black: 63#(<= 0 n1)" "74#true" "15#~initENTRYtrue" "27#~initENTRYtrue" "28#true" "Black: 30#(= critical 0)" "Black: 199#(and (<= 2 n1) (<= (+ n1 1) n0))" "34#true" "Black: 219#(and (<= 2 n1) (<= 1 n0))" "Black: 222#(and (<= 0 n1) (<= 1 n0))" "Black: 36#(<= 1 n1)" "Black: 37#(and (<= 1 n1) (<= (+ n1 1) n0))" "41#true" "Black: 43#(= n0 0)" "Black: 46#(and (<= 1 n1) (<= (+ n1 1) n0))" "50#true" "Black: 52#(<= 1 n1)" "Black: 54#(and (<= 2 n0) (<= (+ n0 1) n1))" "Black: 56#(and (<= 2 n0) (<= 1 n1))" "61#true" }, acceptingPlaces = {"6#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "26#Thread0Err0ASSERT_VIOLATIONASSERTtrue" } ); FiniteAutomaton nwa = ( alphabet = {"assume true;" "n1 := n0 + 1;" "assume n0 == 0 || n1 < n0;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n1 := 0;" "assume !true;" "assume true;" "assume true;" "n0 := n1 + 1;" "assume n1 == 0 || n0 < n1;" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "n0 := 0;" "assume !true;" "assume true;" "critical := 0;n0 := 0;n1 := 1;assume true;" }, states = {"307#(and (<= 0 n0) (<= 1 n1))" "228#true" "309#(and (<= 1 n1) (<= (+ n1 1) n0))" "293#(and (<= (+ n1 1) n0) (<= 3 n1))" "229#false" "230#(<= 0 n0)" "311#(and (<= 2 n0) (<= 3 n1))" "232#(<= 2 n0)" "313#(and (<= 0 n0) (<= 3 n1))" }, initialStates = {"228#true" }, finalStates = {"229#false" }, transitions = { ("307#(and (<= 0 n0) (<= 1 n1))" "assume true;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "n0 := n1 + 1;" "309#(and (<= 1 n1) (<= (+ n1 1) n0))") ("307#(and (<= 0 n0) (<= 1 n1))" "assume true;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "n1 := n0 + 1;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "assume n0 == 0 || n1 < n0;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "assume critical == 0;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "critical := 1;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "critical := 0;" "307#(and (<= 0 n0) (<= 1 n1))") ("307#(and (<= 0 n0) (<= 1 n1))" "n1 := 0;" "230#(<= 0 n0)") ("228#true" "assume true;" "228#true") ("228#true" "n1 := n0 + 1;" "228#true") ("228#true" "assume n0 == 0 || n1 < n0;" "228#true") ("228#true" "assume critical == 0;" "228#true") ("228#true" "critical := 1;" "228#true") ("228#true" "critical := 0;" "228#true") ("228#true" "n1 := 0;" "228#true") ("228#true" "assume n1 == 0 || n0 < n1;" "228#true") ("228#true" "assume critical == 0;" "228#true") ("228#true" "critical := 1;" "228#true") ("228#true" "critical := 0;" "228#true") ("228#true" "n0 := 0;" "230#(<= 0 n0)") ("228#true" "critical := 0;n0 := 0;n1 := 1;assume true;" "307#(and (<= 0 n0) (<= 1 n1))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "assume true;" "309#(and (<= 1 n1) (<= (+ n1 1) n0))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "n1 := n0 + 1;" "311#(and (<= 2 n0) (<= 3 n1))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "assume n0 == 0 || n1 < n0;" "309#(and (<= 1 n1) (<= (+ n1 1) n0))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "assume critical == 0;" "309#(and (<= 1 n1) (<= (+ n1 1) n0))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "critical := 1;" "309#(and (<= 1 n1) (<= (+ n1 1) n0))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "critical := 0;" "309#(and (<= 1 n1) (<= (+ n1 1) n0))") ("309#(and (<= 1 n1) (<= (+ n1 1) n0))" "n1 := 0;" "232#(<= 2 n0)") ("293#(and (<= (+ n1 1) n0) (<= 3 n1))" "assume n1 == 0 || n0 < n1;" "229#false") ("293#(and (<= (+ n1 1) n0) (<= 3 n1))" "assume n0 == 0 || n1 < n0;" "293#(and (<= (+ n1 1) n0) (<= 3 n1))") ("293#(and (<= (+ n1 1) n0) (<= 3 n1))" "assume critical == 0;" "293#(and (<= (+ n1 1) n0) (<= 3 n1))") ("293#(and (<= (+ n1 1) n0) (<= 3 n1))" "critical := 1;" "293#(and (<= (+ n1 1) n0) (<= 3 n1))") ("293#(and (<= (+ n1 1) n0) (<= 3 n1))" "critical := 0;" "293#(and (<= (+ n1 1) n0) (<= 3 n1))") ("293#(and (<= (+ n1 1) n0) (<= 3 n1))" "n1 := 0;" "232#(<= 2 n0)") ("230#(<= 0 n0)" "assume true;" "230#(<= 0 n0)") ("230#(<= 0 n0)" "n0 := n1 + 1;" "228#true") ("230#(<= 0 n0)" "assume true;" "230#(<= 0 n0)") ("230#(<= 0 n0)" "n1 := n0 + 1;" "307#(and (<= 0 n0) (<= 1 n1))") ("230#(<= 0 n0)" "assume n0 == 0 || n1 < n0;" "230#(<= 0 n0)") ("230#(<= 0 n0)" "assume critical == 0;" "230#(<= 0 n0)") ("230#(<= 0 n0)" "critical := 1;" "230#(<= 0 n0)") ("230#(<= 0 n0)" "critical := 0;" "230#(<= 0 n0)") ("230#(<= 0 n0)" "n1 := 0;" "230#(<= 0 n0)") ("311#(and (<= 2 n0) (<= 3 n1))" "assume n1 == 0 || n0 < n1;" "311#(and (<= 2 n0) (<= 3 n1))") ("311#(and (<= 2 n0) (<= 3 n1))" "assume critical == 0;" "311#(and (<= 2 n0) (<= 3 n1))") ("311#(and (<= 2 n0) (<= 3 n1))" "critical := 1;" "311#(and (<= 2 n0) (<= 3 n1))") ("311#(and (<= 2 n0) (<= 3 n1))" "critical := 0;" "311#(and (<= 2 n0) (<= 3 n1))") ("311#(and (<= 2 n0) (<= 3 n1))" "n0 := 0;" "313#(and (<= 0 n0) (<= 3 n1))") ("232#(<= 2 n0)" "assume n1 == 0 || n0 < n1;" "232#(<= 2 n0)") ("232#(<= 2 n0)" "assume true;" "232#(<= 2 n0)") ("232#(<= 2 n0)" "n1 := n0 + 1;" "311#(and (<= 2 n0) (<= 3 n1))") ("232#(<= 2 n0)" "assume critical == 0;" "232#(<= 2 n0)") ("232#(<= 2 n0)" "critical := 1;" "232#(<= 2 n0)") ("232#(<= 2 n0)" "critical := 0;" "232#(<= 2 n0)") ("232#(<= 2 n0)" "n0 := 0;" "230#(<= 0 n0)") ("313#(and (<= 0 n0) (<= 3 n1))" "assume true;" "313#(and (<= 0 n0) (<= 3 n1))") ("313#(and (<= 0 n0) (<= 3 n1))" "n0 := n1 + 1;" "293#(and (<= (+ n1 1) n0) (<= 3 n1))") ("313#(and (<= 0 n0) (<= 3 n1))" "assume n0 == 0 || n1 < n0;" "313#(and (<= 0 n0) (<= 3 n1))") ("313#(and (<= 0 n0) (<= 3 n1))" "assume critical == 0;" "313#(and (<= 0 n0) (<= 3 n1))") ("313#(and (<= 0 n0) (<= 3 n1))" "critical := 1;" "313#(and (<= 0 n0) (<= 3 n1))") ("313#(and (<= 0 n0) (<= 3 n1))" "critical := 0;" "313#(and (<= 0 n0) (<= 3 n1))") ("313#(and (<= 0 n0) (<= 3 n1))" "n1 := 0;" "230#(<= 0 n0)") } );