隱式遷移模型(編輯修改稿)
2024-11-22 09:50 本頁面
【文章內(nèi)容簡介】 )] [l3,(4,2)] [beg,(2,2)] [end,(2,2)] 20 流程圖模型：運行例子 if ?(x=y) goto l2 else goto end if (xy) goto l3 else goto l4 (x):=(xy) goto beg if ?(x=y) goto l2 else goto end if (xy) goto l3 else goto l4 (y):=(yx) goto beg if ?(x=y) goto l2 else goto end 21 流程圖模型：性質(zhì) beg (y):=(yx) (x):=(xy) l2 ?(x=y) xy end l4 l3 yes no yes no x=a, y=b, a?0, b?0 y=gcd(a,b) 22 衛(wèi)式遷移模型 (a=s0) ? (i,j,k,l,a):=(1,0,0,1,s1) (a=s1 ? x=y) ? (a):=(s5) (a=s1 ? ?(x=y)) ? (a):=(s2) (a=s2 ? xy) ? (a):=(s3) (a=s2 ? ?(xy)) ? (a):=(s4) (a=s3) ? (x,i,j,a):=(xy,ik,jl,s1) (a=s4) ? (y,k,l,a):=(yx,ki,lj,s1) 初始狀態(tài)： (a=s0?x?0?y?0) 23 衛(wèi)式遷移模型：例子 24 衛(wèi)式遷移模型：示意圖 (a=s0)? (i,j,k,l,a):=(1,0,0,1,s1) (a=s1?x=y) ? (a):=(s5) (a=s1??(x=y)) ? (a):=(s2) (a=s2?xy) ? (a):=(s3) (a=s2??(xy)) ? (a):=(s4) (a=s3)?(x,i,j,a):=(xy,ik,jl,s1) (a=s4)?(y,k,l,a):=(yx,ki,lj,s1) 初始狀態(tài) : a=s0?x?0?y?0 25 衛(wèi)式遷移模型：示意圖 s5 s0 (a=s0)? (i,j,k,l,a):=(1,0,0,1,s1) (a=s1?x=y) ? (a):=(s5) (a=s1??(x=y)) ? (a):=(s2) (a=s2?xy) ? (a):=(s3) (a=s2??(xy)) ? (a):=(s4) (a=s3)?(x,i,j,a):=(xy,ik,jl,s1) (a=s4)?(
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1