// Benchmark for difference of Petri net and DFA // Generated from // Fischer2unsafe.bpl_AllErrorsAtOnce_Iteration3_AbstractionAfterDifference.ats (2018/07/30 09:54:57) // Fischer2unsafe.bpl_AllErrorsAtOnce_Iteration4_EagerFloydHoareAutomaton.ats (2018/07/30 09:54:57) PetriNet net = ( alphabet = {"#2#assume true;" "#5#assume lock != 2;" "#6#deadline := clk + delay;" "#7#assume lock == 0;" "#8#lock := 2;" "#9#assume clk <= deadline;" "#10#deadline := clk + wait;" "#11#assume clk >= deadline;" "#12#assume lock == 2;" "#14#assume !(lock != 2);" "#16#assume !(critical == 0);" "#17#assume critical == 0;" "#18#critical := 2;" "#19#critical := 0;" "#20#lock := 0;" "#22#assume !true;" "#23#assume true;" "#26#assume true;" "#27#clk := clk + 1;" "#29#assume !true;" "#30#assume true;" "#38#assume true;" "#41#assume lock != 1;" "#42#deadline := clk + delay;" "#43#assume lock == 0;" "#44#lock := 1;" "#45#assume clk <= deadline;" "#46#deadline := clk + wait;" "#47#assume clk >= deadline;" "#48#assume lock == 1;" "#50#assume !(lock != 1);" "#52#assume !(critical == 0);" "#53#assume critical == 0;" "#54#critical := 1;" "#55#critical := 0;" "#56#lock := 0;" "#58#assume !true;" "#59#assume true;" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" }, places = {"5#L79true" "6#L80true" "7#L81true" "8#L82true" "9#Thread2Err0ASSERT_VIOLATIONASSERTtrue" "10#L75-2true" "11#Thread2FINALtrue" "12#L85true" "13#L74true" "14#L75true" "15#L86true" "16#L87true" "17#L76true" "18#L77true" "19#Thread2EXITtrue" "20#L78true" "21#~initENTRYtrue" "23#ClockFINALtrue" "24#ClockEXITtrue" "25#L34true" "26#L35true" "27#~initENTRYtrue" "29#L56true" "30#L57true" "31#L58true" "32#L51-2true" "33#L50true" "34#L61true" "35#L62true" "36#L51true" "37#L52true" "38#Thread1FINALtrue" "39#L63true" "40#L53true" "41#Thread1Err0ASSERT_VIOLATIONASSERTtrue" "42#L54true" "43#Thread1EXITtrue" "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: 58#true" "Black: 60#(<= 2 lock)" }, transitions = { ({"Black: 48#(= critical 0)" "46#true" "15#L86true" } "#19#critical := 0;" {"48#(= critical 0)" "16#L87true" "Black: 46#true" }) ({"52#true" "39#L63true" "Black: 54#(<= lock 1)" "Black: 60#(<= 2 lock)" } "#56#lock := 0;" {"33#L50true" "54#(<= lock 1)" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"18#L77true" "52#true" "Black: 54#(<= lock 1)" "Black: 60#(<= 2 lock)" } "#7#assume lock == 0;" {"20#L78true" "54#(<= lock 1)" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"Black: 46#true" "10#L75-2true" } "#17#assume critical == 0;" {"Black: 46#true" "12#L85true" }) ({"5#L79true" } "#9#assume clk <= deadline;" {"6#L80true" }) ({"20#L78true" "Black: 54#(<= lock 1)" "Black: 58#true" } "#8#lock := 2;" {"5#L79true" "Black: 54#(<= lock 1)" "Black: 58#true" }) ({"44#L55true" } "#45#assume clk <= deadline;" {"29#L56true" }) ({"13#L74true" } "#2#assume true;" {"14#L75true" }) ({"Black: 48#(= critical 0)" "35#L62true" "46#true" } "#55#critical := 0;" {"48#(= critical 0)" "Black: 46#true" "39#L63true" }) ({"Black: 54#(<= lock 1)" "58#true" "14#L75true" "Black: 60#(<= 2 lock)" } "#14#assume !(lock != 2);" {"Black: 54#(<= lock 1)" "10#L75-2true" "60#(<= 2 lock)" "Black: 58#true" }) ({"52#true" "39#L63true" "Black: 54#(<= lock 1)" "60#(<= 2 lock)" "Black: 58#true" } "#56#lock := 0;" {"33#L50true" "54#(<= lock 1)" "Black: 52#true" "58#true" "Black: 60#(<= 2 lock)" }) ({"36#L51true" "Black: 52#true" "Black: 60#(<= 2 lock)" } "#50#assume !(lock != 1);" {"32#L51-2true" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"33#L50true" } "#38#assume true;" {"36#L51true" }) ({"6#L80true" } "#10#deadline := clk + wait;" {"7#L81true" }) ({"Black: 48#(= critical 0)" "10#L75-2true" "46#true" } "#17#assume critical == 0;" {"48#(= critical 0)" "Black: 46#true" "12#L85true" }) ({"8#L82true" "Black: 54#(<= lock 1)" "Black: 58#true" } "#12#assume lock == 2;" {"Black: 54#(<= lock 1)" "10#L75-2true" "Black: 58#true" }) ({"Black: 48#(= critical 0)" "12#L85true" } "#18#critical := 2;" {"Black: 48#(= critical 0)" "15#L86true" }) ({"Black: 52#true" "42#L54true" "Black: 60#(<= 2 lock)" } "#44#lock := 1;" {"Black: 52#true" "44#L55true" "Black: 60#(<= 2 lock)" }) ({"52#true" "40#L53true" "Black: 54#(<= lock 1)" "Black: 60#(<= 2 lock)" } "#43#assume lock == 0;" {"54#(<= lock 1)" "Black: 52#true" "42#L54true" "Black: 60#(<= 2 lock)" }) ({"20#L78true" "54#(<= lock 1)" "Black: 52#true" "Black: 58#true" } "#8#lock := 2;" {"52#true" "5#L79true" "Black: 54#(<= lock 1)" "Black: 58#true" }) ({"32#L51-2true" "Black: 46#true" } "#53#assume critical == 0;" {"34#L61true" "Black: 46#true" }) ({"23#ClockFINALtrue" } "#30#assume true;" {"24#ClockEXITtrue" }) ({"20#L78true" "Black: 54#(<= lock 1)" "58#true" "Black: 60#(<= 2 lock)" } "#8#lock := 2;" {"5#L79true" "Black: 54#(<= lock 1)" "60#(<= 2 lock)" "Black: 58#true" }) ({"16#L87true" "Black: 52#true" "Black: 60#(<= 2 lock)" } "#20#lock := 0;" {"Black: 52#true" "13#L74true" "Black: 60#(<= 2 lock)" }) ({"7#L81true" } "#11#assume clk >= deadline;" {"8#L82true" }) ({"34#L61true" "Black: 48#(= critical 0)" } "#54#critical := 1;" {"Black: 48#(= critical 0)" "35#L62true" }) ({"Black: 52#true" "42#L54true" "60#(<= 2 lock)" "Black: 58#true" } "#44#lock := 1;" {"Black: 52#true" "58#true" "44#L55true" "Black: 60#(<= 2 lock)" }) ({"14#L75true" } "#5#assume lock != 2;" {"17#L76true" }) ({"8#L82true" "Black: 54#(<= lock 1)" "58#true" "Black: 60#(<= 2 lock)" } "#12#assume lock == 2;" {"Black: 54#(<= lock 1)" "10#L75-2true" "60#(<= 2 lock)" "Black: 58#true" }) ({"52#true" "36#L51true" "Black: 54#(<= lock 1)" "Black: 60#(<= 2 lock)" } "#50#assume !(lock != 1);" {"32#L51-2true" "54#(<= lock 1)" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"32#L51-2true" "Black: 48#(= critical 0)" "46#true" } "#53#assume critical == 0;" {"48#(= critical 0)" "34#L61true" "Black: 46#true" }) ({"32#L51-2true" "Black: 48#(= critical 0)" } "#52#assume !(critical == 0);" {"Black: 48#(= critical 0)" "41#Thread1Err0ASSERT_VIOLATIONASSERTtrue" }) ({"16#L87true" "Black: 52#true" "60#(<= 2 lock)" "Black: 58#true" } "#20#lock := 0;" {"Black: 52#true" "58#true" "13#L74true" "Black: 60#(<= 2 lock)" }) ({"25#L34true" } "#26#assume true;" {"26#L35true" }) ({"20#L78true" "54#(<= lock 1)" "Black: 52#true" "58#true" "Black: 60#(<= 2 lock)" } "#8#lock := 2;" {"52#true" "5#L79true" "Black: 54#(<= lock 1)" "60#(<= 2 lock)" "Black: 58#true" }) ({"38#Thread1FINALtrue" } "#59#assume true;" {"43#Thread1EXITtrue" }) ({"Black: 52#true" "31#L58true" "Black: 60#(<= 2 lock)" } "#48#assume lock == 1;" {"32#L51-2true" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"52#true" "Black: 54#(<= lock 1)" "42#L54true" "Black: 60#(<= 2 lock)" } "#44#lock := 1;" {"54#(<= lock 1)" "Black: 52#true" "44#L55true" "Black: 60#(<= 2 lock)" }) ({"26#L35true" } "#27#clk := clk + 1;" {"25#L34true" }) ({"36#L51true" } "#41#assume lock != 1;" {"37#L52true" }) ({"29#L56true" } "#46#deadline := clk + wait;" {"30#L57true" }) ({"39#L63true" "Black: 52#true" "Black: 60#(<= 2 lock)" } "#56#lock := 0;" {"33#L50true" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"18#L77true" "Black: 52#true" "Black: 60#(<= 2 lock)" } "#7#assume lock == 0;" {"20#L78true" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"11#Thread2FINALtrue" } "#23#assume true;" {"19#Thread2EXITtrue" }) ({"Black: 48#(= critical 0)" "10#L75-2true" } "#16#assume !(critical == 0);" {"Black: 48#(= critical 0)" "9#Thread2Err0ASSERT_VIOLATIONASSERTtrue" }) ({"Black: 46#true" "21#~initENTRYtrue" "27#~initENTRYtrue" "45#~initENTRYtrue" } "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" {"33#L50true" "Black: 46#true" "25#L34true" "13#L74true" }) ({"16#L87true" "52#true" "Black: 54#(<= lock 1)" "Black: 60#(<= 2 lock)" } "#20#lock := 0;" {"54#(<= lock 1)" "Black: 52#true" "13#L74true" "Black: 60#(<= 2 lock)" }) ({"48#(= critical 0)" "Black: 46#true" "12#L85true" } "#18#critical := 2;" {"Black: 48#(= critical 0)" "46#true" "15#L86true" }) ({"52#true" "Black: 54#(<= lock 1)" "42#L54true" "60#(<= 2 lock)" "Black: 58#true" } "#44#lock := 1;" {"54#(<= lock 1)" "Black: 52#true" "58#true" "44#L55true" "Black: 60#(<= 2 lock)" }) ({"Black: 46#true" "15#L86true" } "#19#critical := 0;" {"16#L87true" "Black: 46#true" }) ({"39#L63true" "Black: 52#true" "60#(<= 2 lock)" "Black: 58#true" } "#56#lock := 0;" {"33#L50true" "Black: 52#true" "58#true" "Black: 60#(<= 2 lock)" }) ({"30#L57true" } "#47#assume clk >= deadline;" {"31#L58true" }) ({"17#L76true" } "#6#deadline := clk + delay;" {"18#L77true" }) ({"Black: 54#(<= lock 1)" "14#L75true" "Black: 58#true" } "#14#assume !(lock != 2);" {"Black: 54#(<= lock 1)" "10#L75-2true" "Black: 58#true" }) ({"16#L87true" "52#true" "Black: 54#(<= lock 1)" "60#(<= 2 lock)" "Black: 58#true" } "#20#lock := 0;" {"54#(<= lock 1)" "Black: 52#true" "58#true" "13#L74true" "Black: 60#(<= 2 lock)" }) ({"Black: 48#(= critical 0)" "21#~initENTRYtrue" "27#~initENTRYtrue" "45#~initENTRYtrue" "46#true" } "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" {"48#(= critical 0)" "33#L50true" "Black: 46#true" "25#L34true" "13#L74true" }) ({"37#L52true" } "#42#deadline := clk + delay;" {"40#L53true" }) ({"48#(= critical 0)" "34#L61true" "Black: 46#true" } "#54#critical := 1;" {"Black: 48#(= critical 0)" "35#L62true" "46#true" }) ({"35#L62true" "Black: 46#true" } "#55#critical := 0;" {"Black: 46#true" "39#L63true" }) ({"52#true" "Black: 54#(<= lock 1)" "31#L58true" "Black: 60#(<= 2 lock)" } "#48#assume lock == 1;" {"32#L51-2true" "54#(<= lock 1)" "Black: 52#true" "Black: 60#(<= 2 lock)" }) ({"40#L53true" "Black: 52#true" "Black: 60#(<= 2 lock)" } "#43#assume lock == 0;" {"Black: 52#true" "42#L54true" "Black: 60#(<= 2 lock)" }) }, initialMarking = {"Black: 48#(= critical 0)" "52#true" "21#~initENTRYtrue" "Black: 54#(<= lock 1)" "58#true" "27#~initENTRYtrue" "45#~initENTRYtrue" "46#true" "Black: 60#(<= 2 lock)" }, acceptingPlaces = {"9#Thread2Err0ASSERT_VIOLATIONASSERTtrue" "41#Thread1Err0ASSERT_VIOLATIONASSERTtrue" } ); FiniteAutomaton nwa = ( alphabet = {"#2#assume true;" "#5#assume lock != 2;" "#6#deadline := clk + delay;" "#7#assume lock == 0;" "#8#lock := 2;" "#9#assume clk <= deadline;" "#10#deadline := clk + wait;" "#11#assume clk >= deadline;" "#12#assume lock == 2;" "#14#assume !(lock != 2);" "#16#assume !(critical == 0);" "#17#assume critical == 0;" "#18#critical := 2;" "#19#critical := 0;" "#20#lock := 0;" "#22#assume !true;" "#23#assume true;" "#26#assume true;" "#27#clk := clk + 1;" "#29#assume !true;" "#30#assume true;" "#38#assume true;" "#41#assume lock != 1;" "#42#deadline := clk + delay;" "#43#assume lock == 0;" "#44#lock := 1;" "#45#assume clk <= deadline;" "#46#deadline := clk + wait;" "#47#assume clk >= deadline;" "#48#assume lock == 1;" "#50#assume !(lock != 1);" "#52#assume !(critical == 0);" "#53#assume critical == 0;" "#54#critical := 1;" "#55#critical := 0;" "#56#lock := 0;" "#58#assume !true;" "#59#assume true;" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" }, states = {"64#true" "65#false" "66#(<= lock 0)" }, initialStates = {"64#true" }, finalStates = {"65#false" }, transitions = { ("64#true" "#2#assume true;" "64#true") ("64#true" "#5#assume lock != 2;" "64#true") ("64#true" "#6#deadline := clk + delay;" "64#true") ("64#true" "#7#assume lock == 0;" "66#(<= lock 0)") ("64#true" "#8#lock := 2;" "64#true") ("64#true" "#9#assume clk <= deadline;" "64#true") ("64#true" "#10#deadline := clk + wait;" "64#true") ("64#true" "#11#assume clk >= deadline;" "64#true") ("64#true" "#12#assume lock == 2;" "64#true") ("64#true" "#14#assume !(lock != 2);" "64#true") ("64#true" "#16#assume !(critical == 0);" "64#true") ("64#true" "#17#assume critical == 0;" "64#true") ("64#true" "#18#critical := 2;" "64#true") ("64#true" "#19#critical := 0;" "64#true") ("64#true" "#20#lock := 0;" "66#(<= lock 0)") ("64#true" "#22#assume !true;" "65#false") ("64#true" "#23#assume true;" "64#true") ("64#true" "#26#assume true;" "64#true") ("64#true" "#27#clk := clk + 1;" "64#true") ("64#true" "#29#assume !true;" "65#false") ("64#true" "#30#assume true;" "64#true") ("64#true" "#38#assume true;" "64#true") ("64#true" "#41#assume lock != 1;" "64#true") ("64#true" "#42#deadline := clk + delay;" "64#true") ("64#true" "#43#assume lock == 0;" "66#(<= lock 0)") ("64#true" "#44#lock := 1;" "64#true") ("64#true" "#45#assume clk <= deadline;" "64#true") ("64#true" "#46#deadline := clk + wait;" "64#true") ("64#true" "#47#assume clk >= deadline;" "64#true") ("64#true" "#48#assume lock == 1;" "64#true") ("64#true" "#50#assume !(lock != 1);" "64#true") ("64#true" "#52#assume !(critical == 0);" "64#true") ("64#true" "#53#assume critical == 0;" "64#true") ("64#true" "#54#critical := 1;" "64#true") ("64#true" "#55#critical := 0;" "64#true") ("64#true" "#56#lock := 0;" "66#(<= lock 0)") ("64#true" "#58#assume !true;" "65#false") ("64#true" "#59#assume true;" "64#true") ("64#true" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" "64#true") ("65#false" "#2#assume true;" "65#false") ("65#false" "#5#assume lock != 2;" "65#false") ("65#false" "#6#deadline := clk + delay;" "65#false") ("65#false" "#7#assume lock == 0;" "65#false") ("65#false" "#8#lock := 2;" "65#false") ("65#false" "#9#assume clk <= deadline;" "65#false") ("65#false" "#10#deadline := clk + wait;" "65#false") ("65#false" "#11#assume clk >= deadline;" "65#false") ("65#false" "#12#assume lock == 2;" "65#false") ("65#false" "#14#assume !(lock != 2);" "65#false") ("65#false" "#16#assume !(critical == 0);" "65#false") ("65#false" "#17#assume critical == 0;" "65#false") ("65#false" "#18#critical := 2;" "65#false") ("65#false" "#19#critical := 0;" "65#false") ("65#false" "#20#lock := 0;" "65#false") ("65#false" "#22#assume !true;" "65#false") ("65#false" "#23#assume true;" "65#false") ("65#false" "#26#assume true;" "65#false") ("65#false" "#27#clk := clk + 1;" "65#false") ("65#false" "#29#assume !true;" "65#false") ("65#false" "#30#assume true;" "65#false") ("65#false" "#38#assume true;" "65#false") ("65#false" "#41#assume lock != 1;" "65#false") ("65#false" "#42#deadline := clk + delay;" "65#false") ("65#false" "#43#assume lock == 0;" "65#false") ("65#false" "#44#lock := 1;" "65#false") ("65#false" "#45#assume clk <= deadline;" "65#false") ("65#false" "#46#deadline := clk + wait;" "65#false") ("65#false" "#47#assume clk >= deadline;" "65#false") ("65#false" "#48#assume lock == 1;" "65#false") ("65#false" "#50#assume !(lock != 1);" "65#false") ("65#false" "#52#assume !(critical == 0);" "65#false") ("65#false" "#53#assume critical == 0;" "65#false") ("65#false" "#54#critical := 1;" "65#false") ("65#false" "#55#critical := 0;" "65#false") ("65#false" "#56#lock := 0;" "65#false") ("65#false" "#58#assume !true;" "65#false") ("65#false" "#59#assume true;" "65#false") ("65#false" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" "65#false") ("66#(<= lock 0)" "#2#assume true;" "66#(<= lock 0)") ("66#(<= lock 0)" "#5#assume lock != 2;" "66#(<= lock 0)") ("66#(<= lock 0)" "#6#deadline := clk + delay;" "66#(<= lock 0)") ("66#(<= lock 0)" "#7#assume lock == 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#8#lock := 2;" "64#true") ("66#(<= lock 0)" "#9#assume clk <= deadline;" "66#(<= lock 0)") ("66#(<= lock 0)" "#10#deadline := clk + wait;" "66#(<= lock 0)") ("66#(<= lock 0)" "#11#assume clk >= deadline;" "66#(<= lock 0)") ("66#(<= lock 0)" "#12#assume lock == 2;" "65#false") ("66#(<= lock 0)" "#14#assume !(lock != 2);" "65#false") ("66#(<= lock 0)" "#16#assume !(critical == 0);" "66#(<= lock 0)") ("66#(<= lock 0)" "#17#assume critical == 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#18#critical := 2;" "66#(<= lock 0)") ("66#(<= lock 0)" "#19#critical := 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#20#lock := 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#22#assume !true;" "65#false") ("66#(<= lock 0)" "#23#assume true;" "66#(<= lock 0)") ("66#(<= lock 0)" "#26#assume true;" "66#(<= lock 0)") ("66#(<= lock 0)" "#27#clk := clk + 1;" "66#(<= lock 0)") ("66#(<= lock 0)" "#29#assume !true;" "65#false") ("66#(<= lock 0)" "#30#assume true;" "66#(<= lock 0)") ("66#(<= lock 0)" "#38#assume true;" "66#(<= lock 0)") ("66#(<= lock 0)" "#41#assume lock != 1;" "66#(<= lock 0)") ("66#(<= lock 0)" "#42#deadline := clk + delay;" "66#(<= lock 0)") ("66#(<= lock 0)" "#43#assume lock == 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#44#lock := 1;" "64#true") ("66#(<= lock 0)" "#45#assume clk <= deadline;" "66#(<= lock 0)") ("66#(<= lock 0)" "#46#deadline := clk + wait;" "66#(<= lock 0)") ("66#(<= lock 0)" "#47#assume clk >= deadline;" "66#(<= lock 0)") ("66#(<= lock 0)" "#48#assume lock == 1;" "65#false") ("66#(<= lock 0)" "#50#assume !(lock != 1);" "65#false") ("66#(<= lock 0)" "#52#assume !(critical == 0);" "66#(<= lock 0)") ("66#(<= lock 0)" "#53#assume critical == 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#54#critical := 1;" "66#(<= lock 0)") ("66#(<= lock 0)" "#55#critical := 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#56#lock := 0;" "66#(<= lock 0)") ("66#(<= lock 0)" "#58#assume !true;" "65#false") ("66#(<= lock 0)" "#59#assume true;" "66#(<= lock 0)") ("66#(<= lock 0)" "critical := 0;clk := 0;assume wait >= 1;assume wait >= delay;assume true;" "66#(<= lock 0)") } );