[MUSIC] Nice to see you again. In this lecture I will take another exercise of the VerifyThis competition that took place in London in 2015 and model it and analyze its correctness. So, if you have two numbers, then the greatest common divisor is the number that divides both numbers, and there’s not a larger number that also divides both numbers. So if you have 4 and 6, then the greatest common divisor is 2. If we have 10 and 4, it may take a little longer, but you will see that 2 is the greatest common divisor of these two numbers. And the question is, how can we calculate that? Well, there's a simple algorithm for that, namely, you take both numbers and you subtract the smallest from the largest. And then you repeat this process until both numbers become equal, and it will always happen after a finite number of steps. Applying that to 10 and 4 means 4 is smallest. As we subtract 4 from 10, we get 6 and 4. We subtract 4 again from 6, we get 2 and 4. We subtract 2 from 4, we get 2 and 2. And they have become equal, and that means that 2 is the smallest common divisor of 10 and 4. It's important to note that this is a nice and simple algorithm but not an extremely efficient algorithm. So in this VerifyThis competition, the question was, if we start to calculate this in parallel, is the answer then still correct? So you have two threads. And the first thread is written down here. It does the following. As long as a and b are not equal, that are the numbers to which we apply the algorithm. And if a is larger than b, then we replace a by a-b. And the other thread does the same, except that it checks whether b is larger than a. And if so, it replaces b by b-a. If both values a and b have become equal, then we simply output a. So how can we model this? We do this as follows, we take two actions. And we make a simple model, so I avoid parallelism. And in the next lecture, I will show that that can always be done. Parallelism does not really add something to behavior. We have these two actions, step 1 and step 2. Step 1 means, the first process, or the first thread, makes a step. Step 2 means the second process makes a step, and we have this report action. And a report action delivers true if the resulting common divisor, if the result is really the common divisor of the input, and otherwise it reports false. So how can we model this process? We have four parameters of the process. The first two parameters are the values a and b that we also saw in the parallel process, in the parallel algorithm. The two other values a0 and b0 are the initial values, and we need them to check whether an answer is correct. So if we take the first thread, if a is larger than b, then we can do a step 1 action and replace a by a-b. And what we see here is the so-called assignment notation that I have not yet explained up till now. But it says that we only change the value of the parameter a of the process and leave all other parameters intact. In the same way, we can do a step of the second process mainly if b is larger than a. Then we replace b by b-a. And if the values of a and b have become the same, then we simply report whether a is the greatest common divisor of a0 and b0. And that is what the function GCD expresses. If you want to verify that this protocol works in a correct way, we cannot do that with modal checking for all initial failures. But what we can do is we can take value a from a certain range, so smaller than a certain maximum and a value b, smaller than a certain maximum and check it for all these a's and b's. And if we take MAX of a reasonable value, then it's quite unlikely that we will overlook that the algorithm is incorrect because it behaves the same for most input values anyhow. Our experience is that errors, that if you check it for a decent input range, then this is a very good indicator of the correctness. Although, theoretically you should probably prove the correctness by hand, but it will take vastly more time. Okay, we have still this predicate GCD. And we want to formulate it in a very natural way such that you are convinced that it is indeed expressing correctly that an input value is the greatest common divider. So we have the values a, b, and g. When is g the greatest common divisor of a and b? Well, g should divide a, so a modulo g should be = 0. g should be a divisor of b, so b modulo g = 0. And for every candidate x that is larger than g, it should not be the greatest common divisor anymore. So, we find that either g(x) is not dividing a. And x is not dividing b. And what we do here in this formulation, is that we limit x to the maximum of a and b because we know that if x is larger, then it will certainly not be a common divisor of both. But this also allows us to calculate this universal quantification. Otherwise, the tools cannot handle with this universal quantification and this point. So now the question is, when is this algorithm actually correct? And it's always difficult to find the correct requirement of any system. In this particular case, we suggested the following tool. Whenever a result is being delivered, it should be correct. And the other property is that results are always delivered. So if these two properties hold, then we believe we have a correctly working parallel algorithm for the GCD. So how can we formulate the first property? We want that if we have a report action, then we should always report true, namely a should be the greatest common devisor of a0 and b0. We may never, ever see a report false. And that last property is formulated as a modal formula in this way. So whenever we see a report false, we end up in a state where false holds, or in other words, report false cannot occur in the reachable part of our state space. If we look at the second property, then we want to say that the results are delivered. So on every part of our system within a finite number of steps, report must happen. So what we want to say, and I think you now recognize this formula immediately. Is that report happens unavoidably on every pass, independent of what it is actually reporting, so we use this typical minimal fixed point for that. And now I think we should have a look at how the tools are verifying this. And we can show there that both formulas are actually valid for our formulation of this problem. So here we see the directory with our input files in parallel_gcd.mcrl2. We find our input algorithm. And in correct.mcf, we find our correctness formula. And in delivered.mcf, we find the formula that says we can always terminate the algorithm. So how do we verify that? We need to transform Our process into a linear process specification, which is done this way. So we now have this parallel, or the linear process specification available. We can use the tool, lps2pbes, to make a parameterized boolean equation system for a formula correct. And now we generate this parameter as boolean equation system. There are two ways to solve it. We have here pbes2bool or pbespgsolve. We select pbes2bool or pbespgsolve, it's very useful if you have alternating fixed points. And we prefer to use the compiling rewriter, which is available on the Mac and on Linux, unfortunately not on the Windows machine. And we can check the formula. And you see here that the rewrite system is being compiled. And now the system checks whether the formula was true, and we see that the answer is indeed true. In the same way, we can check the delivered formula. We already prepared a parameterized boolean equation system for that, and we can again apply pbes2bool to it. Let's do it again with the compile and rewrite. And what you can see is that also this formula actually holds. So let's look at an exercise. Now that we have a first model of our algorithm we can make changes. And one of the changes is that in the original formulation, we have this skip. So if we look at the first trait, and if we have a not larger than b in the first trait, then it does escape an original formulation. So we can add that to our formulation in this way by simply adding the skip action. And then the question is, if you look at the properties that we have formulated, are they still valid? And as a side note, you may not know this notation. But this notation is actually the empty assignment notation. And X with two brackets without any content means we do not update any argument, or the parameters of the process simply remain unchanged. So what did we do? We took this simple algorithm to calculate the greatest common divisor in parallel, and we made a model for that. We formulated a correctness and a termination property, and we translated that to modal formulas. And we checked that for our formulation both formulas were true. In the next lecture we will look at the workhorse for all the tools, and that is a linear process specification. Thank you for watching. [MUSIC]