Cadence SMV Vending Machine 김그린김바울
INDEX 1. Problem Analysis 2. Modeling 3. Model Checking
1. Problem Analysis Default Money Inserted Count Money Reject Money Cancel Give Change Default Not Enough Money Cancel Enough Money Select Beverage & Coffee Selected Dispense Not Selected
1. Problem Analysis Money Inserted input_money total_money Count Money Default Reject Money Cancel Not Enough Money Give Change in_50,in_100,in_500,in_1000 out_50,out_100,out_500,out_1000 Cancel Default no,apple_can,beer_can,coke_can water,coffeepowder,sugar,cream Enough Money refund_button,apple_button.beer_button Coke_button,drpepper_button apple,beer,coke,drpepper,energy Select Beverage & Coffee Selected Dispense black,sugar,cream,milk,max Not Selected
1. Problem Analysis money dispense input_money : {input_0,input_50,input_100,input_500,input_1000}; total_money :{0,50,100,150,200,250,300,350,400,450,500,550,600,650,700,750,800,850,900,950,1000,1050,1100,1150,1200,1250, 1300,1350,1400,1450,1500,1550,1600,1650,1700,1750,1800,1850,1900,1950,2000,2050,2100,2150,2200,2250,2300,2350,2400,245 0,2500,2550,2600,2650,2700,2750,2800,2850,2900,2950,3000,3050,3100,3150,3200,3250,3300,3350,3400,3450,3500,3550,3600,3 650,3700,3750,3800,3850,3900,3950,4000,4050,4100,4150,4200,4250,4300,4350,4400,4450,4500,4550,4600,4650,4700,4750,4800,4850,4900,4950,5000}; in_50,out_50 :{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,4 1,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83, 84,85,86,87,88,89,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100}; in_100,out_100 : {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,4 6,47,48,49,50}; in_500,out_500 : {0,1,2,3,4,5,6,7,8,9,10}; in_1000,out_1000 : {0,1,2,3,4,5}; dispense : {no,apple_can,beer_can,coke_can,drpepper_can,energy_can,black_cup,sugar_cup, cream_cup,milk_cup,max_cup} display button stock apple_display : {on,off,out_of_stock} beer_display: {on,off,out_of_stock} coke_display : {on,off,out_of_stock} drpepper_display: {on,off,out_of_stock}; energy_display : {on,off,out_of_stock}; black_display : {on,off,out_of_stock}; sugar_display : {on,off,out_of_stock}; cream_display : {on,off,out_of_stock}; milk_display : {on,off,out_of_stock}; max_display : {on,off,out_of_stock}; lamp : boolean; extra_display : {money_display,water_display}; input_button :{no,refund,apple,beer,coke,drpeppe r,energy,black,sugar,cream,milk,max}; refund_button : boolean; apple_button : boolean; beer_button : boolean; coke_button : boolean; drpepper_button : boolean; energy_button : boolean; black_button : boolean; sugar_button : boolean; cream_button : boolean; milk_button : boolean; max_button : boolean; apple_stock : {0,1,2,3,4,5,6,7,8,9,10}; beer_stock : {0,1,2,3,4,5,6,7,8,9,10}; coke_stock : {0,1,2,3,4,5,6,7,8,9,10}; drpepper_stock : {0,1,2,3,4,5,6,7,8,9,10}; energy_stock : {0,1,2,3,4,5,6,7,8,9,10}; water_stock : {0,1,2,3,4,5,6,7,8,9,10}; coffeepowder_stock : {0,1,2,3,4,5,6,7,8,9,10}; sugar_stock : {0,1,2,3,4,5,6,7,8,9,10}; cream_stock : {0,1,2,3,4,5,6,7,8,9,10};
2. Modeling 50 550 1050 4550 4050 3550 3050 2550 2050 1550 500 1000 1500 5000 4500 4000 3500 3000 2500 2000 100 600 1100 4600 4100 3600 3100 2600 2100 1600 150 650 1150 4650 4150 3650 3150 2650 2150 1650 200 700 1200 4700 4200 3700 3200 2700 2200 1700 250 750 1250 4750 4250 3750 3250 2750 2250 1750 300 800 1300 4800 4300 3800 3300 2800 2300 1800 350 850 1350 4850 4350 3850 3350 2850 2350 1850 400 900 1400 4900 4400 3900 3400 2900 2400 1900 450 950 1450 4950 4450 3950 3450 2950 2450 1950 input_0 input_50 input_1000 input_500 input_100 apple_button
2. Modeling input_0 input_50 input_100 input_500 input_1000 apple_button 50 100 500 1000 next(total_money) := total_money +0 next(in_50) := in_50 +1 next(total_money) := total_money +50 next(in_100) := in_100 + 1 next(total_money) := total_money +100 next(in_500) := in_500 +1 next(total_money) := total_money +500 next(in_1000) := in_1000 + 1 next(total_money) := total_money +1000 total_money 500 && apple_stock 1 total_money 500 && beer_stock 1 total_money 300 && coffeepower_stock 1&&water_stock 1 &&sugar_stock 1&&cream_stock 1&&cup_stock 1 next(apple_displa y) := on next(beer_display) := on next(milk_coffee) := on next(max_coffee) := on
2. Modeling next(apple_displa y) := on next(beer_display) := on next(milk_coffee) := on next(max_coffee) := on Default next(display) := on or off out_of_stock next(dispense) := can or cup next(total_money) := total_money - price next(stock) := stock - 1 refund_button next(display) := off or out_of_stock next(total_money) := 0 next(in_50) := 0
test1 : Assert G(total_money = 3600 & input_money=input_500&refund_button=0 -> X(total_money=4100)); test2 : Assert G(total_money = 3600 & input_button=apple & refund_button=0 & input_money=input_500 -> X(total_money=4100)); test3 : Assert G(total_money = 3600 & input_button=apple & input_button=drpepper -> X(dispense=apple_can & dispense=drpepper_can)); test4 : Assert G(total_money = 3600 & input_button=apple & refund_button=1 -> X(dispense=apple_can & total_money=0)); test5 : Assert G(total_money = 3600 & input_button=black & input_button=max -> X(dispense=black_cup & dispense=max_cup));
test6 : Assert G(total_money = 3600 & apple_display=on & apple_stock=0 -> X(apple_display = out_of_stock)); test7 : Assert G(total_money = 600 & input_button=apple & apple_display=on & refund_button=1 -> X(apple_display = off)); test8 : Assert G(total_money = 1000 & refund_button=1 -> X(out_1000 = 1)); test9 : Assert G(total_money = 600 & apple_button=1 & refund_button=1 -> X(out_100 = 1 & dispense=apple_can)); test10 : Assert G(total_money = 600 & max_button=1 & coffeepowder_stock > 1 & water_stock > 1 & cream_stock > 1 & sugar_stock = 0 -> X(dispense~=max_cup));
test1 : Assert G(total_money = 3600 & input_money=input_500&refund_button=0 -> X(total_money=4100));
test2 : Assert G(total_money = 3600 & input_button=apple & refund_button=0 & input_money=input_500 -> X(total_money=4100));
test3 : Assert G(total_money = 3600 & input_button=apple & input_button=drpepper -> X(dispense=apple_can & dispense=drpepper_can));
test4 : Assert G(total_money = 3600 & input_button=apple & refund_button=1 -> X(dispense=apple_can & total_money=0));
test5 : Assert G(total_money = 3600 & input_button=black & input_button=max -> X(dispense=black_cup & dispense=max_cup));
test6 : Assert G(total_money = 3600 & apple_display=on & apple_stock=0 -> X(apple_display = out_of_stock));
test7 : Assert G(total_money = 600 & input_button=apple & apple_display=on & refund_button=1 -> X(apple_display = off));
test8 : Assert G(total_money = 1000 & refund_button=1 -> X(out_1000 = 1));
test9 : Assert G(total_money = 600 & apple_button=1 & refund_button=1 -> X(out_100 = 1 & dispense=apple_can));
test10 : Assert G(total_money = 600 & max_button=1 & coffeepowder_stock > 1 & water_stock > 1 & cream_stock > 1 & sugar_stock = 0 -> X(dispense~=max_cup));
Any question? Thank you