Assignment8-2 WhileEnd

[HyeongMee]

I solved the problem 8-2 til it appeared like below :

WHILE BLe (ANum 0) (AId X) DO Y ::= APlus (AId Y) (AId X);; X ::= AMinus (AId X) (ANum 1) END) / update (update (update (update (update (update empty_state X 2) Y 0) Y 2) X 1) Y 3) X 0 || update (update (update (update (update (update empty_state X 2) Y 0) Y 2) X 1) Y 3) X 0

So I thought that i had to apply WhileEnd, but then realized that it couldn't work 'cuz BLe is 'less or equal'. (- that's right?? I guess? ) But then How can I make it terminate? I tried below one as well to solve this problem ;

apply E_WhileEnd. with (st := (update (update (update (update (update (update (update empty_state X 2) Y 0) Y 2) X 1) Y 3) X 0) X (aeval (update empty_state X 0) (AMinus (AId X) (ANum 1))))).

but I feel like it's not right 'cuz it led to another deadlock (- I felt that to be a deadlock ;;)

Then what should I do?

Thanks!! :D

[jeehoonkang]

Would you please enclose code by escaping characters https://help.github.com/articles/github-flavored-markdown/ ? Thanks!

[jaewooklee93]

WHILE BLe (ANum 0) (AId X) ~ never terminates, because there is no negative number until now.

I think your definition of pup_to_n was already wrong, so think about it again.

[HyeongMee]

@jeehoonkang Okay I will do that from now on 'cuz I solved this problem ! Thnaks :D @jaewooklee93 That really was the problem. Thanks a million.