PowerPoint 프레젠테이션

Size: px

Start display at page:

Download "PowerPoint 프레젠테이션"

주형 교
5 years ago
Views:

1 Cadence SMV Vending Machine 김그린김바울

2 INDEX 1. Problem Analysis 2. Modeling 3. Model Checking

3 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

4 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

5 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};

6 2. Modeling input_0 input_50 input_1000 input_500 input_100 apple_button

7 2. Modeling input_0 input_50 input_100 input_500 input_1000 apple_button next(total_money) := total_money +0 next(in_50) := in_50 +1 next(total_money) := total_money +50 next(in_100) := in_ next(total_money) := total_money +100 next(in_500) := in_ next(total_money) := total_money +500 next(in_1000) := in_ next(total_money) := total_money 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

8 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

9 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));

10 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));

11 test1 : Assert G(total_money = 3600 & input_money=input_500&refund_button=0 -> X(total_money=4100));

12 test2 : Assert G(total_money = 3600 & input_button=apple & refund_button=0 & input_money=input_500 -> X(total_money=4100));

13 test3 : Assert G(total_money = 3600 & input_button=apple & input_button=drpepper -> X(dispense=apple_can & dispense=drpepper_can));

14 test4 : Assert G(total_money = 3600 & input_button=apple & refund_button=1 -> X(dispense=apple_can & total_money=0));

15 test5 : Assert G(total_money = 3600 & input_button=black & input_button=max -> X(dispense=black_cup & dispense=max_cup));

16 test6 : Assert G(total_money = 3600 & apple_display=on & apple_stock=0 -> X(apple_display = out_of_stock));

17 test7 : Assert G(total_money = 600 & input_button=apple & apple_display=on & refund_button=1 -> X(apple_display = off));

18 test8 : Assert G(total_money = 1000 & refund_button=1 -> X(out_1000 = 1));

19 test9 : Assert G(total_money = 600 & apple_button=1 & refund_button=1 -> X(out_100 = 1 & dispense=apple_can));

20 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));

21 Any question? Thank you

<FEFF11121162110211611106116E002D1107116911B71112116900330036002E0069006E0064006400000000000093782FC816B427590034001CBDFC1B558B202E6559E830EB00000000937C28D9>

<FEFF11121162110211611106116E002D1107116911B71112116900330036002E0069006E0064006400000000000093782FC816B427590034001CBDFC1B558B202E6559E830EB00000000937C28D9> 02 04 06 14 16 19 24 26 27 28 31 3 4 5 세상과 (소통)하다!! 세상과 (소통)하다!! 세상과 (소통)하다!! 6 7 건강지원 프로그램으로 굳어져가는 몸과 마음을 풀어보아요~ 8 9 새해 복 많이 받으세요~ 10 11 12 13 14 15 14 14 14 14 15 15 16 17 18 19 20 21 방과 후 교실(해나무 주간보호센터