// Benchmark for difference of Petri net and DFA // Generated from // Fischer2safe.bpl_AllErrorsAtOnce_Iteration7_AbstractionAfterDifference.ats (2018/08/13 05:05:29) // Fischer2safe.bpl_AllErrorsAtOnce_Iteration8_EagerFloydHoareAutomaton.ats (2018/08/13 05:05:32) PetriNet net = ( alphabet = {"assume true;" "assume lock != 2;" "deadline := clk + delay;" "assume lock == 0;" "lock := 2;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 2;" "assume !(lock != 2);" "assume !(critical == 0);" "assume critical == 0;" "critical := 2;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "assume true;" "clk := clk + 1;" "assume !true;" "assume true;" "assume true;" "assume lock != 1;" "deadline := clk + delay;" "assume lock == 0;" "lock := 1;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 1;" "assume !(lock != 1);" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "critical := 0;clk := 0;assume wait >= 1;assume wait > delay;assume true;" }, places = {"5#L79true" "6#L80true" "7#L81true" "8#Thread2Err0ASSERT_VIOLATIONASSERTtrue" "9#L82true" "10#L75-2true" "12#L85true" "13#L74true" "14#L75true" "15#L86true" "16#L87true" "17#L76true" "18#L77true" "20#L78true" "21#~initENTRYtrue" "25#L34true" "26#L35true" "27#~initENTRYtrue" "29#L56true" "30#L57true" "31#L58true" "32#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "33#L51-2true" "34#L50true" "35#L61true" "36#L62true" "37#L51true" "38#L52true" "40#L63true" "41#L53true" "42#L54true" "44#L55true" "45#~initENTRYtrue" "46#true" "48#(= critical 0)" "Black: 48#(= critical 0)" "Black: 46#true" "52#true" "54#(<= lock 1)" "Black: 52#true" "Black: 54#(<= lock 1)" "58#true" "60#(<= 2 lock)" "Black: 60#(<= 2 lock)" "63#true" "65#(<= 1 lock)" "Black: 65#(<= 1 lock)" "Black: 63#true" "69#true" "71#(<= lock 0)" "Black: 69#true" "Black: 71#(<= lock 0)" "75#true" "77#(<= 1 wait)" "80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "83#true" "85#(<= (+ delay 1) wait)" "90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" }, transitions = { ({"Black: 48#(= critical 0)" "46#true" "15#L86true" } "critical := 0;" {"48#(= critical 0)" "16#L87true" "Black: 46#true" }) ({"Black: 65#(<= 1 lock)" "20#L78true" "54#(<= lock 1)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "58#true" "Black: 60#(<= 2 lock)" "63#true" } "lock := 2;" {"65#(<= 1 lock)" "Black: 63#true" "52#true" "69#true" "5#L79true" "Black: 54#(<= lock 1)" "Black: 71#(<= lock 0)" "60#(<= 2 lock)" }) ({"Black: 46#true" "10#L75-2true" } "assume critical == 0;" {"Black: 46#true" "12#L85true" }) ({"18#L77true" "Black: 65#(<= 1 lock)" "52#true" "69#true" "Black: 54#(<= lock 1)" "Black: 71#(<= lock 0)" } "assume lock == 0;" {"Black: 65#(<= 1 lock)" "20#L78true" "54#(<= lock 1)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" }) ({"Black: 65#(<= 1 lock)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "42#L54true" "Black: 60#(<= 2 lock)" "63#true" } "lock := 1;" {"65#(<= 1 lock)" "Black: 63#true" "69#true" "Black: 52#true" "Black: 71#(<= lock 0)" "44#L55true" "Black: 60#(<= 2 lock)" }) ({"48#(= critical 0)" "Black: 46#true" "35#L61true" } "critical := 1;" {"Black: 48#(= critical 0)" "36#L62true" "46#true" }) ({"Black: 46#true" "36#L62true" } "critical := 0;" {"Black: 46#true" "40#L63true" }) ({"16#L87true" "Black: 65#(<= 1 lock)" "Black: 52#true" "Black: 69#true" "Black: 60#(<= 2 lock)" } "lock := 0;" {"Black: 65#(<= 1 lock)" "Black: 52#true" "Black: 69#true" "13#L74true" "Black: 60#(<= 2 lock)" }) ({"92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "29#L56true" } "deadline := clk + wait;" {"Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "85#(<= (+ delay 1) wait)" "30#L57true" }) ({"17#L76true" "Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" } "deadline := clk + delay;" {"96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "18#L77true" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" }) ({"13#L74true" } "assume true;" {"14#L75true" }) ({"33#L51-2true" "Black: 48#(= critical 0)" } "assume !(critical == 0);" {"32#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "Black: 48#(= critical 0)" }) ({"Black: 65#(<= 1 lock)" "Black: 54#(<= lock 1)" "58#true" "Black: 60#(<= 2 lock)" "14#L75true" "63#true" } "assume !(lock != 2);" {"65#(<= 1 lock)" "Black: 63#true" "Black: 54#(<= lock 1)" "10#L75-2true" "60#(<= 2 lock)" }) ({"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "44#L55true" } "assume clk <= deadline;" {"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "29#L56true" }) ({"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "6#L80true" "77#(<= 1 wait)" } "deadline := clk + wait;" {"80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "7#L81true" }) ({"Black: 48#(= critical 0)" "10#L75-2true" "46#true" } "assume critical == 0;" {"48#(= critical 0)" "Black: 46#true" "12#L85true" }) ({"16#L87true" "65#(<= 1 lock)" "Black: 63#true" "69#true" "Black: 52#true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" } "lock := 0;" {"Black: 65#(<= 1 lock)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "13#L74true" "Black: 60#(<= 2 lock)" "63#true" }) ({"Black: 48#(= critical 0)" "12#L85true" } "critical := 2;" {"Black: 48#(= critical 0)" "15#L86true" }) ({"20#L78true" "Black: 63#true" "54#(<= lock 1)" "Black: 52#true" "58#true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" } "lock := 2;" {"52#true" "Black: 63#true" "5#L79true" "Black: 54#(<= lock 1)" "Black: 71#(<= lock 0)" "60#(<= 2 lock)" }) ({"Black: 48#(= critical 0)" "36#L62true" "46#true" } "critical := 0;" {"48#(= critical 0)" "Black: 46#true" "40#L63true" }) ({"Black: 52#true" "41#L53true" "Black: 69#true" "Black: 60#(<= 2 lock)" } "assume lock == 0;" {"Black: 52#true" "Black: 69#true" "42#L54true" "Black: 60#(<= 2 lock)" }) ({"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "5#L79true" } "assume clk <= deadline;" {"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "6#L80true" }) ({"34#L50true" } "assume true;" {"37#L51true" }) ({"29#L56true" "94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" } "deadline := clk + wait;" {"85#(<= (+ delay 1) wait)" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "30#L57true" }) ({"96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "29#L56true" } "deadline := clk + wait;" {"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "85#(<= (+ delay 1) wait)" "30#L57true" }) ({"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "26#L35true" } "clk := clk + 1;" {"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "25#L34true" }) ({"80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "26#L35true" } "clk := clk + 1;" {"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "25#L34true" "77#(<= 1 wait)" }) ({"14#L75true" } "assume lock != 2;" {"17#L76true" }) ({"33#L51-2true" "Black: 46#true" } "assume critical == 0;" {"35#L61true" "Black: 46#true" }) ({"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "7#L81true" "92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" } "assume clk >= deadline;" {"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "9#L82true" "94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" }) ({"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "6#L80true" "90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "77#(<= 1 wait)" } "deadline := clk + wait;" {"80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "7#L81true" "92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" }) ({"Black: 65#(<= 1 lock)" "40#L63true" "Black: 52#true" "Black: 69#true" "Black: 60#(<= 2 lock)" } "lock := 0;" {"34#L50true" "Black: 65#(<= 1 lock)" "Black: 52#true" "Black: 69#true" "Black: 60#(<= 2 lock)" }) ({"Black: 65#(<= 1 lock)" "52#true" "37#L51true" "Black: 54#(<= lock 1)" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" "63#true" } "assume !(lock != 1);" {"65#(<= 1 lock)" "33#L51-2true" "Black: 63#true" "54#(<= lock 1)" "Black: 52#true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" }) ({"96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "5#L79true" } "assume clk <= deadline;" {"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "6#L80true" "94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" }) ({"16#L87true" "65#(<= 1 lock)" "Black: 63#true" "52#true" "69#true" "Black: 54#(<= lock 1)" "Black: 71#(<= lock 0)" "60#(<= 2 lock)" } "lock := 0;" {"Black: 65#(<= 1 lock)" "54#(<= lock 1)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "58#true" "13#L74true" "Black: 60#(<= 2 lock)" "63#true" }) ({"25#L34true" } "assume true;" {"26#L35true" }) ({"Black: 48#(= critical 0)" "35#L61true" } "critical := 1;" {"Black: 48#(= critical 0)" "36#L62true" }) ({"17#L76true" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" } "deadline := clk + delay;" {"18#L77true" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" }) ({"52#true" "Black: 63#true" "Black: 54#(<= lock 1)" "42#L54true" "Black: 71#(<= lock 0)" "60#(<= 2 lock)" } "lock := 1;" {"Black: 63#true" "54#(<= lock 1)" "Black: 52#true" "58#true" "Black: 71#(<= lock 0)" "44#L55true" "Black: 60#(<= 2 lock)" }) ({"Black: 48#(= critical 0)" "10#L75-2true" } "assume !(critical == 0);" {"Black: 48#(= critical 0)" "8#Thread2Err0ASSERT_VIOLATIONASSERTtrue" }) ({"52#true" "69#true" "Black: 54#(<= lock 1)" "41#L53true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" } "assume lock == 0;" {"54#(<= lock 1)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "42#L54true" "Black: 60#(<= 2 lock)" }) ({"9#L82true" "Black: 54#(<= lock 1)" } "assume lock == 2;" {"Black: 54#(<= lock 1)" "10#L75-2true" }) ({"33#L51-2true" "Black: 48#(= critical 0)" "46#true" } "assume critical == 0;" {"48#(= critical 0)" "Black: 46#true" "35#L61true" }) ({"65#(<= 1 lock)" "Black: 63#true" "69#true" "40#L63true" "Black: 52#true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" } "lock := 0;" {"34#L50true" "Black: 65#(<= 1 lock)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "Black: 60#(<= 2 lock)" "63#true" }) ({"Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "85#(<= (+ delay 1) wait)" "38#L52true" } "deadline := clk + delay;" {"41#L53true" "90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" }) ({"Black: 63#true" "Black: 52#true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" "31#L58true" } "assume lock == 1;" {"33#L51-2true" "Black: 63#true" "Black: 52#true" "Black: 71#(<= lock 0)" "Black: 60#(<= 2 lock)" }) ({"18#L77true" "Black: 65#(<= 1 lock)" "Black: 52#true" "Black: 69#true" } "assume lock == 0;" {"Black: 65#(<= 1 lock)" "20#L78true" "Black: 52#true" "Black: 69#true" }) ({"48#(= critical 0)" "Black: 46#true" "12#L85true" } "critical := 2;" {"Black: 48#(= critical 0)" "46#true" "15#L86true" }) ({"37#L51true" } "assume lock != 1;" {"38#L52true" }) ({"Black: 46#true" "15#L86true" } "critical := 0;" {"16#L87true" "Black: 46#true" }) ({"30#L57true" } "assume clk >= deadline;" {"31#L58true" }) ({"Black: 48#(= critical 0)" "83#true" "21#~initENTRYtrue" "75#true" "27#~initENTRYtrue" "45#~initENTRYtrue" "46#true" } "critical := 0;clk := 0;assume wait >= 1;assume wait > delay;assume true;" {"48#(= critical 0)" "34#L50true" "Black: 46#true" "85#(<= (+ delay 1) wait)" "25#L34true" "77#(<= 1 wait)" "13#L74true" }) ({"90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "29#L56true" } "deadline := clk + wait;" {"Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "85#(<= (+ delay 1) wait)" "30#L57true" }) ({"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "7#L81true" } "assume clk >= deadline;" {"Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "9#L82true" }) ({"65#(<= 1 lock)" "Black: 63#true" "52#true" "69#true" "40#L63true" "Black: 54#(<= lock 1)" "Black: 71#(<= lock 0)" "60#(<= 2 lock)" } "lock := 0;" {"34#L50true" "Black: 65#(<= 1 lock)" "54#(<= lock 1)" "71#(<= lock 0)" "Black: 52#true" "Black: 69#true" "58#true" "Black: 60#(<= 2 lock)" "63#true" }) }, initialMarking = {"Black: 96#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 65#(<= 1 lock)" "Black: 90#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 92#(and (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "69#true" "Black: 94#(and (<= (+ Thread1_deadline 1) clk) (<= (+ delay 1) wait) (<= (+ Thread1_deadline 1) Thread2_deadline) (<= (+ Thread1_deadline 1) (+ wait clk)))" "Black: 71#(<= lock 0)" "75#true" "45#~initENTRYtrue" "46#true" "Black: 48#(= critical 0)" "Black: 80#(and (<= 1 wait) (<= (+ clk 1) Thread2_deadline))" "83#true" "52#true" "21#~initENTRYtrue" "Black: 54#(<= lock 1)" "58#true" "27#~initENTRYtrue" "Black: 60#(<= 2 lock)" "63#true" }, acceptingPlaces = {"32#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "8#Thread2Err0ASSERT_VIOLATIONASSERTtrue" } ); FiniteAutomaton nwa = ( alphabet = {"assume true;" "assume lock != 2;" "deadline := clk + delay;" "assume lock == 0;" "lock := 2;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 2;" "assume !(lock != 2);" "assume !(critical == 0);" "assume critical == 0;" "critical := 2;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "assume true;" "clk := clk + 1;" "assume !true;" "assume true;" "assume true;" "assume lock != 1;" "deadline := clk + delay;" "assume lock == 0;" "lock := 1;" "assume clk <= deadline;" "deadline := clk + wait;" "assume clk >= deadline;" "assume lock == 1;" "assume !(lock != 1);" "assume !(critical == 0);" "assume critical == 0;" "critical := 1;" "critical := 0;" "lock := 0;" "assume !true;" "assume true;" "critical := 0;clk := 0;assume wait >= 1;assume wait > delay;assume true;" }, states = {"102#true" "103#false" "104#(<= 1 wait)" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" }, initialStates = {"102#true" }, finalStates = {"103#false" }, transitions = { ("102#true" "critical := 0;clk := 0;assume wait >= 1;assume wait > delay;assume true;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume true;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume lock != 2;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "deadline := clk + delay;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume lock == 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "lock := 2;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume clk <= deadline;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "deadline := clk + wait;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume clk >= deadline;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume lock == 2;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume !(lock != 2);" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume !(critical == 0);" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume critical == 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "critical := 2;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "critical := 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "lock := 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume true;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "clk := clk + 1;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume true;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume lock != 1;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "deadline := clk + delay;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume lock == 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "lock := 1;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume clk <= deadline;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "deadline := clk + wait;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("104#(<= 1 wait)" "assume clk >= deadline;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume lock == 1;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume !(lock != 1);" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume !(critical == 0);" "104#(<= 1 wait)") ("104#(<= 1 wait)" "assume critical == 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "critical := 1;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "critical := 0;" "104#(<= 1 wait)") ("104#(<= 1 wait)" "lock := 0;" "104#(<= 1 wait)") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume true;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume lock != 2;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "deadline := clk + delay;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume lock == 0;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "lock := 2;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume clk <= deadline;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "deadline := clk + wait;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume clk >= deadline;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume lock == 2;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume clk >= deadline;" "103#false") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume critical == 0;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "critical := 2;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "critical := 0;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "lock := 0;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "assume true;" "107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))") ("107#(and (<= (+ clk 1) Thread1_deadline) (<= 1 wait))" "clk := clk + 1;" "104#(<= 1 wait)") } );