OK, welcome back. Let's wait a few more seconds.
Interestingly enough, we have a clear, favorite or not a clear favorite, but one answer is 16.
And the other one has 11:10 and 6:00.
So let's review what we have and then mcy.
The.
So the correct answers are two and sweet.
OK, so that's the 1st and the absurd.
One that was picked also picked was 12.
OK.
No wait, F is 7, seven was picked.
12 was picked and and one was picked. OK, so let's.
Try to work out what's going on, and let's maybe do it.
By drawing.
Let's take the time to do that so.
Uhm?
What's going on?
The tablet is not working.
Does it work?
No.
OK, don't let me see.
Alright, here we go. OK so we.
Initialize X, so this means excess value 0 at the beginning. Remember that I said that variables are initialized to value zero. Let me get rid of my video so that we have the full thing. OK, so the variable is initialized to zero. And now if we switch back to the slides, we have two.
Guards here in the next if statement that is executed X is equal to 0 or X is equal to 1 and.
Only the first guard is.
Enabled because the second one evaluates to false. Zero the value of X is not equal to 1, right? So what will happen is we will assign the value of 1 to X.
So after the first if let me write it like that.
We have X is equal to 1.
And now let's switch back to the slides.
There are two activated guards, the first one and the second one because X has indeed value one. The last two are not activated. So what will happen? Miss Nondeterministically one of the two statements will be executed, so we either add.
22 MX.
Or we multiply X by two. OK, so let's switch back.
So we either end up at.
X is equal to three. That's when we add 2.
Or we end up at X is equal to two. This is the second option when we multiply X by two OK.
These are the two options that can happen, and these are exactly the answers. PNC OK?
Does it make sense?
So.
Again, as this is non deterministic choice, there's not a unique value that access at the after this.
Code fragment there are multiple possibilities. OK depending on which statement is picked.
And so these are not deterministic programs like your typical Java or C program.
But you have this nondeterminism in there. OK, so for us what I want to do now is I wanna let me switch to.
The program, but I want to do is now use such a statement too.
Select some values for.
The variable, so I say a is equal to 14 for example, or a is equal to 27.
Or a is equal to 77?
Or A is groups.
This way a is equal to 123 and what will happen is after this selection statement has been executed, a has one of these four values. OK because again they have no guard. I might as well write true.
This is equivalent.
But yeah, it's bit more verbose, so let's remove this.
One of the four options is picked Nondeterministically and then we continue here. So let me copy this and.
Also, nondeterministically assign some value to.
Be whatever.
What 68 OK, so one of the four values is picked for a, B and now what I want to do is I want to also give some output. So let me copy this in.
Groups
so this is a print statement. This will be just printed to the console and this year. Wait, I have to put it afterwards because I want to output the value of a. So this year just prints this text here and the.
Percentage sign and then you just means a print the.
Value of the variable as an unsigned integer and the variable I just specify after the string as a parameter after the comma. OK so I wanna give some output and the same for the B so that I can read off which values have been picked.
So here I give the value of B and I print it.
And that's now my process generator. It picks some value for a from this list, it picks a value for B from this list Prince what it has picked and some additional tax, and then it terminates. OK, this is how we can use.
The selection statement would nondeterministically pick and input from a list of options.
OK.
The next thing I want to introduce is the repetition statement. OK, there was a question. Let's go back.
What is the percent sign with you mean it means it's a placeholder, like in many programming languages. If you want to print the value of a variable, you just write percentage you.
And then in the place of that keyword, the value of a B will be printed and then you just signifies that it's treated as an unsigned of integer OK.
Let's just run it to find out.
Let me just turn off all these things so that it's a bit less.
Verde
so.
This is the output.
You get the value of the variable age. This will be 27.
Add the value picked for a.
The Derby this is for the sweet and annoyingly the sweet. Here is an output generated by the program which says sweet processes were created. OK, so if I add here a space then we will at least.
Have a.
The space here. I could also add a slash and this should give us a new line. Then it looks even better.
No, I have to run it so the the city of 14 and 68 and then I get the next message on the next line. OK, so again the percentage you just means take the value of the variable that is specified afterwards and print it in this place.
OK.
And you can use this several times and then just list several variables afterwards if necessary, OK?
So let's move on.
Turn.
The next thing.
Uh.
To do what? If there are some characters still?
Do tell you can use different things. They are documented in the manual on spinward. OK, I'm not 100% sure what the right keywords are, so if you need this.
Please look it up but.
I guess for what we are doing this year will be enough.
But if it does something strange, if you need a signed integer, for example because you work with negative numbers, then look it up.
OK, good so after we have seen a sort of if then else statement or not deterministic one, the next thing you wanna do is you wanna repeat something you want to have loops right? And for this we have the repetition statement looks very similar to the selection statement, you just use the keyboard do and for the opening start and opt for the closing bracket at the end.
But otherwise it looks completely similar. You have the guards and you have these blocks of code that are executed then.
But the semantics is different. What is going on is now we do this repeatedly when we arrive here we look at which guards are enabled.
One of those will not deterministically picked the sequence of statements induced by that will be executed.
And then we go back to the start and pick again. One of the guards that is activated and then continue like that forever and in each iteration in you choice is made. So it might be the case that.
The option one is executed in the first iteration, then option two in the second one and then option one again at maybe a force in the first iteration. Again, option one and so on.
From the.
Guards that are enabled. You pick one of them nondeterministically and then execute this option. This subsequence of quote afterwards, OK?
Add.
You are.
Half the break statement. This is a keyword to leave this ibloop this arm repetition statement. So if you execute a break in one of these code blocks then you will get to the end of the repetition block and continue afterwards. OK, there's one more option. There's also jump statement which can take you out of such repetition. This we will see later. OK, but.
As you might have already seen, jumps are considered to be very dangerous because they lead to unreadable code and unvented maintainable code. So the better thing to do is to use a break statement whenever possible.
OK, so let's again see an example. So what I do now is I have the.
Count variable again.
And now I have this repetition statement here and either.
Am I increment count and this doesn't have a guard, so this is possible in every iteration.
Also, in every iteration I can decrement the count.
Or if the count is equal to zero, I can also leave this loop here. OK, So what will happen is I nondeterministically increase or decrease.
The value of count.
Until it is, I terminate.
But this I only do whether count is equal to 0. But, crucially, notice that the increment and decrement are always enabled.
Even if the value of count is zero. OK, so it might be the case that count is zero and I increment it to one.
And then I decrement it and then it's zero, but I still do not terminate. Leave the loop. Instead I decremented by one OK.
Please.
Take this piece of code and play around with the simulator to understand the meaning or the semantics of this on repetition here and try also to write it in a way that ensures that when the value is 0 then I leave the loop OK. This is a good exercise.
But again.
I may terminate when the count is equal to 0, but I don't have to. I can use one of the other two statements if I want.
OK.
So.
Let's actually here is the we find example. So yeah, why not talk about it if I have it, what I do is the following I do.
Distinguish with two guards whether the count is not equal to 0, or if it's equal to 0. If it's equal that I break, or if it's not equal, then I have this.
Select block now which either increments or decrements. OK, so this is how it looks like.
If you want to.
Have it in a way that you have to terminate at zero OK, But there's still this unknown determinism. If you are not sure whether you increment or decrement that still around.
OK, so let's see what's on the next slide. OK, let's finish this before we move back to the program.
You can implement now for example a while loop. Do think using this.
This repetition construct very similar to what we did with the if then else you just write if.
The value of A is strictly smaller than the value of B. Then I decrement the B and if this is not the case then I break. So what will now happen is the value of B will be decremented as long as it is. I'm strictly bigger than a.
OK, so if the value of B is strictly greater than the value of a before we arrive at the do statement, then we will have that a is equal to B is true after the two statement because I decrement the value of B until they are equal.
But if B is not strictly greater than a before the new statement, then it will be left immediately and A&B are left unchanged OK.
Because then immediately only this Guardian is enabled, which means I will break and leave the loop immediately.
And this is essentially a while loop. You can also implement for loops and other types of loops with very similar logic. You just have to explicitly write down the two conditions and make sure that exactly one of them is applicable at any time. Then you have a deterministic loop implemented OK.
Good so.
Let's move back to the program. I'm aware that I'm using again a bit more time, so I'm sorry about that, but let's.
Quickly see how to use this.
So.
Let's try to write the Euclid's algorithm.
So if you remember what it does, it's a loop.
That has two things.
Or don't know, I guess sweet. Let me look on my CHEAT SHEET.
Yeah, we have two options we have. If a is greater than B.
So A is a greater one. So what we do is we.
Subtract the smaller one from the larger one. This leaves me with a positive number and then we have the dual case. If B is greater than a, then what we do is we.
Substr act, subtract, get groups the smaller from the bigger one. Is this correct?
Today, yes.
And finally, if they are equal.
Then
or the door sweep, wait OK. Now this will compute. This is Euclids algorithm computing the GCD.
Of A&B what I want to add here is I want to make sure that the generator has picked.
Values for RA&B.
And the way I do this is by using the unblocking statements. So remember that this statement can only be executed.
If a is greater than zero, which means since a is initialized with zero, that generator has picked a value for.
A.
And similarly this year can only be executed if generators picked the value for be OK, and then we run the algorithm and then we just I'm given output and let me just copy this.
To speed things up.
So now I print the value of A and this should be the GCD.
So let's run this and hope for the best. Of course, as expected, we have a syntax error. I can't have a space there.
And now it says the GCD of 123 and 68 is 1.
So they don't share a divisor but one.
And let's see.
68 is
34 * 2 is 17 * 2 * 2 and 123 is divisible by sweetz 61.
How to do 61 prime number?
Might be right.
Not 100% sure if somebody knows whether 61 is a prime number, let me know, but this seems to be OK, so let's run something again. Hopefully something simpler. 77 and 66. The GCD is 11. This I can believe it 'cause this is 7 * 11 and this is 2 * 3 * 11. So this looks good. Let's do one more thing.
The GCD of 27 and 68 is 127 is 3 * 3 * 3 and 68 is.
Again, 4 * 17, so it should be one, so this looks good. Seems to be doing the job, so this is a very simple.
Program in promela.
And you cannot run it. You can also put in other values.
If you want to, you can write your own program and yeah, we will later see what else we can do, but that's it for what we learn today. I just want to mention one more thing before we conclude.
We have already seen that what the interleaving semantics mean. Practically, we have all these processes running in parallel and.
If several statements are enabled.
Then either one of them is pick nondeterministically.
Or if you run the simulation, you can pick which one you want to simulate. You have to pick one of them. OK, if you just press the run button, then dice is thrown and one of them is a picked that are enabled. So in general, if you have something like this year, we have prototyped a which just increments X and we have the init which runs A and then multiplies X Byam 2. Then after we have run a now boasts.
I'm of the statements are enabled, the multiplication by two and the increment of X.
And so.
This is not deterministic choice. Which one to execute 1st and then the other statement is executed?
And what that means is.
At termination, the value of the shared variable X is either four in the upper branch order. It is sweet at the lower branch and now either the scheduler determines which branch is taking. This was the run button. Then just randomly one of the choices is picked. Or if you run the interactive simulation then you can pick which one is some chosen OK.
And finally, later when we do verification, then every possible branch is evaluated OK because we want to be sure that no matter how the program behaves, it satisfies in specification. OK, so this is something we always have to keep in mind. These interleaving semantics. It's always just one statement that is executed, and if several ones are enabled then there is nondeterminism. OK, we will see later why this non determinism is crucial.
But for the time being, we just have to remember this when we write programs.
OK, so this is what I just said repeated. We can simulate. Then we have the scheduler randomly picking and enable transition or we can have the interactive simulation. Then the user determines the schedule and this is useful to understanding what your program does OK.
So let's conclude here. As said tomorrow we will be introducing up channels and a few other features.
For today, that's it. If you have questions, please feel free to ask them and let me conclude by mentioning that I am uploaded. The discussion of the second class test. The videos are available on the module page all the way at the bottom, and you should also have access to your.
Class test results. If you haven't done so, please check them. You should be able to see your answers in the correct answers. If anybody has problems with accessing them, I'm still learning how to deal with Canvas then please just let me know and I will look into this OK.
Thanks everybody and see you tomorrow at 10.
Bye.