All right. So, we're on to workshop six. So, this is going to be quite a complicated workshop and we're going to make use of predicates, which of course was the topic of this week. So, here is our starting model, where we've got the maximum time allowed, the guards, the food, the water. And already we've thought a bit about the model, because these decisions are very reasonably clever, right? We know that for the correct weighing, no food or water should disappear. So, we're just going to move the food and water back and forth. So we can just say F is moving, if it's a positive number, it's moving it from the bank to the boat; a negative number from the boat to the bank. We don't need to keep track of anything else. We are going to need to keep track of how much food is on the boat. >> Right. >> Right? So we're going to have an array. Well, I'm going to introduce another index set TIME0. From 0 to T, we've seen this kind of thing before, because when we're keeping track of the position of the elephant; the state of this system, we're going to have a start state, which is 0, and then we're going to have the state after any number of steps. So these are going to be indexed by TIME0, so what am I going to keep track of? Well, I'm going to keep track of how much food is on the boat? Right? The food on the boat, and I have to keep track of… This is the sneakiness, I could keep track of how much food is on the bank as well, but since the food never changes, it's either on the boat or on the bank, I can actually work out how much food is on the bank by just subtracting the amount I started off with. This from that amount. So I'm going to also need to keep track of… >> But that's assuming that the elephant will not eat any of them. >> Yeah, but remember. >> [LAUGH] >> If the elephant eats, then we're wrong. The weighing’s not going to work. So the other thing we're going to have to keep track of is where is the elephant, right? >> Right. So, I think, this is not a bad place to use an enumerated type. Right? So, these are positions, and then we're going to have the time. Where is the elephant at each time? Let's call it pos. >> Okay, so these are some auxiliary things that we going to have to keep track of in this model. And then possibly the most complicated thing is sort of trying to work out, first of all, does the elephant move? >> Yeah. >> Because we're going to have to force them to move to the boat, at least once. So this is a good thing for a predicate, right? So, does the elephant move? >> Right. >> So now we can do this a number of ways. Let's just do it this way. Let's say we can look at. There's some amount of food where the elephant is. So that's meant to be the food, let's call it the fhere (food here). Right. And there's some amount of water where the elephant is. And there's also some amount of food where the elephant isn't. And some amount of water, where the elephant isn't. Except that where w is not going to work. Let's call it wthere (water). And wrthere (water there). >> Yeah. >> All right. So, remember our rules for the elephant to move was… Actually, I prefer the equals there. We needed that, the water and the food at the other place is equal, right? So, that's wtthere. Yeah, that's very confusing. Let's call it wr, because otherwise I'm going to get very confused. So the wrthere = fthere. >> Yep. >> So that first. And (/\), we also need to be more things over there. >> Yeah. >> So fthere > fhere. And (/\) the wrthere > wrhere. All right, so that's going to say that the elephant moves. >> Actually, for the definition here, do we really need the last two parameters in there? >> That's true, we could actually do the calculation >> exactly. Actually, that's a good idea. Let's do it differently. So we'll look at what is here. We could do it separately. >> Yeah. >> By saying let and we can introduce these. >> Yes. >> As local variables. So, the fthere, we know is, in fact, F - fhere. >> Yup. And the wrthere is W - wrhere. Oops, that equals goes there. Yeah, so we could do it that way instead. All right. So, that's when the elephant moves. We need to keep track of the state of everything, right? So, let's do those constraints, because those, well. Let's do the start state. What do we know is true initially? >> Initially. >> So, we know that the position of the elephant at time zero is the bank. >> On the bank, yeah. >> Yeah. We know that the food on the boat at
time zero, fboat[0], is zero, right? >> Yep. >> And we know that the water on the boat, >> Is also 0. >> at time zero, wboat[0], is zero, right? And then we've got these constraints about updating these things. So, we update, let's update the food first. So, forall(t in TIME), right? The food on the boat at time t, fboat[t], is equal to move_food. Remember, positive is moving to the boat. >> Yeah. >> + fboat[t-1] Yeah? >> Yup. >> And we do a similar thing for the water. >> Yeah. >> So this is going to keep track of how things …change. All right, so the elephant’s, more complicated. But we’ve got some restrictions, right? We can only move a certain amount. So, we should also keep track of that. So each time, obviously we can only move up to G things. Right. So, the abs(move_food [t]), oops, + abs( move_water[t]) <= the number of guards we have to move things. That was a very unfortunate line break. But we can only move things in one direction. So, how are we going to model that? So an obvious way is to say something like (if move_food[t] > 0 then move_water[t] >= 0 >> Yup. >> Yup. else true. endif, right? >> Yeah. >> Just to finish off the endif and we need the other case as well. If move_food[t] < 0 (so if we're moving food backwards) then move_water[t] <= 0. Right. >> Yeah. >> That's one way of doing it, but actually, we can do it a bit better way than that. So basically, a different way of doing that would be to say this. If we take move_food[t] and multiply it by move_water[t], it has to be greater than or equal to 0, right? So if one of them's 0 we know we can move the other one in any direction. >> Yeah. >> But otherwise they both have to be the same sign. >> This is much cleaner. >> Yes, and that should produce faster solving in most solvers. >> Yeah. >> Not guaranteed. It's multiplying two numbers together and some solvers don't like that so much. But whatever happens, it's certainly cleaner than that. All right. So, I think the only thing we have left to talk about now is getting this elephant to move. Right? So basically, we have to work out what to do with the elephant. So I think this is also worth talking about. Let's make a predicate that's going to keep track of the elephant's behavior. Right? So. This is where it is now. >> Yeah. >> Let's say this is the food. So if we look at our example here, we want to know what the food is here, right? So this is the food with the elephant, yep? >> Yep. >> And this is the water, yes this is the- >> wr. >> wr. Water with the elephant and what we want to work out is where does the elephant get to? Right. >> New position, yeah. >> Let’s call it next. >> Yeah. >> All right- >> We should have a capital W over there. >> Capital W, thank you. So, basically, we can think about it this if the elephant moves, right. And now, we have the data we need for that, which is just fhere and wrhere. Yeah, then...what happens?, so the next is equal to, well, the opposite of now, all right. if now = Bank then Boat else Bank. >> Yeah. >> Otherwise, next = now. So we can do that, but actually, this is a common thing. If we see an if then else with two definitions of a variable, we really should try and push this test inside the definition of the variable. >> Right. >> Okay. Because that will make, basically this is a disjunction and pushing the disjunctions in further is going to be more efficient. So we can rewrite that instead by saying, well next = and actually we can do another trick too which is here, right, we're just trying to reverse the position. Why don't we build an array of positions, which gives us the opposite, right? Which is Boat, Bank. >> Yeah. >> Yup. So now we're going to… If the elephant moves then it moves to the opposite of now. Yeah? Actually, if it doesn't move, let's say it this way. It stays where it is, otherwise it moves to the opposite of now. That's an array. Yep? And I can look that up, mm-hm, with this move variable. >> This is really, really tricky. >> [LAUGH] Yeah. >> Wow. >> Okay, we have to add one, because the index is here on one and two. So, this says if the elephant moves, then this will evaluate to two, which means I'll get the opposite position. And if it doesn't move, it'll evaluate to one, which I'll give the current position. >> Wow. >> Okay, so this form of the constraint is likely to be much more efficient because basically, the disjunction is sort of hidden here. We can get some information about next regardless of knowing which decision is made, right? We don’t get much information in this particular case, but this kind of idea is very useful, typically. So now we have to finally actually assert this thing and this is something which we haven't done here. Which is, we're always talking about the food here and the water here so we're going to have to actually work out those values. So, we have to set up this elephant constraint to work out where the elephant goes. So if… So we can do similar things. Let's do it this way. So let's work out the fhere. That's with the elephant. Right, so we can. That is going to be either the fboat, right. Or F- fboat at this time. >> Mm-hm. >> Yeah. >> So if the elephant's on the bank, actually, so it’s the other way around. F-fboat. So if the elephant's on the bank, then we want this. If the elephant's on the boat, we want that. So we can actually just take the position of the elephant and look it up. >> So we're using the same trick? >> Exactly. Except we’ve got a terrible line break there. Let's bring that back and we can do the same for the water. Right. It's = [W - wboat[t], and otherwise wboat[t]. And use the elephant position to look up that array. And now we're ready, we're missing open brace there for our loop, to apply our elephant predicate, right? So we take the position of t- 1. We take the fhere, which we just ripped out and the wrhere and then we get the pos[t]. Right? And. So, we need to workout the end condition, right. So, we succeed. So, remember that we're trying to, we want… Where's it gone? The endtime. >> Yep. >> So, at the end time, what do we know? Well, we know the position of the elephant is on the boat and the fboat = 0. >> 0. >> Yep. >> Yep. >> So we can do the accurate measurement and the wboat = 0. Let’s try solve minimize end, but there's one thing we've forgotten, actually. >> Yeah. >> Which is that, Jimmy? Do you remember? >> After the last step, after we have done the measurement of the weight of the elephant, then there will be no further movement of the water and the food. >> We can add constraints saying that. So forall (t in TIME), I’d forgotten about that one. Because there's still another one. If t > end -> move_water… so this is really actually just going to reduce the possibilities, cause we don't want to think about moving water and food around after we've succeeded. >> This is actually a common trick that we would use to model a plan of >> unknown length. Right? >> Yeah exactly. >> And we would like to minimize the end time, right? >> Yeah. So we try to minimize the end time and so we're trying to make sure that after the end time, nothing happens automatically. >> Right. >> All right. We've actually missed one thing, which is the we have to stop the elephant from eating. >> Right. >> Now we have all the information we need to determine that here right? We know how much food is there and how much water is there. So basically we just need to add need another constraint here which says that the fhere = 0 <-> where wrhere = 0. Okay. Yeah. >> Okay. So, we're going to add… because this is enough to stop the elephant eating. So, if one of them is empty, so, it would eat the other one or drink the other one. But, this will make sure, it can't. Either there's both food and water or there is none of them either. >> Right. >> Or we can add that into our elephant behaviour constraint. And I think that's probably enough. So let's load some data. So there’s our test data which will run. Ooh. And of course we have forgotten something. So, in this forall (t in TIME), what is missing? >> Should be a simple sentence there. >> Yeah it’s just close braces. Undefined wboat so obviously I've called it something else. fboat and fwater, well that doesn't make much sense. [LAUGH] >> [LAUGH] >> It's meant to be wboat. >> Yeah. >> Let's make sure that we used wboat everywhere else we did. All right, so that was just an error. Undefined identifier 'move'. So I used move in here. I've used braces instead of… So these are the kinds of errors we get used to making and hopefully… All right, we can see the plan. It’s a bit hard to see there because we're outputting so many things. We move three, what's the data here? This doesn't look very good to me. >> Nope. >> We move three food, and then we moved it back. And we ended at 10. That's very strange. Solve minimize end. All right, so what is going on? Why don't we take the answer that we wrote that expect here and add it in? Yeah, right. Let's do some debugging. So we expect >> 0, 3. >> 3, >> -2, -1, and then six 0s. >> So this is the answer that we were given. >> 3, 0. -1, -2, and then six 0s. You're seeing real time debugging here. It's a real debugging. >> [LAUGH] >> end = 4. Okay. >> Okay. We get unsatisfiable, and now we can start to say, okay, what constraint is… That's true we could put the end as well. >> Equal to four. >> So what is causing that to fail? So, it's got to be… Something in our… In this elephant I'm thinking. fhere, wrhere. Just make sure the position is correct. Bank boat, yep. So that's looking like the right values. So 3 can only move to the last moment which doesn't make any sense either. So the move is definitely wrong. So let's look at our move definition. Okay, or looking up so let's look at our move definition. So the fthere = F - fhere, W - wrhere. This all looks good to me. That's the reason to move. All right, well if you comment out this one, how do you do the quick comments? >> Just select all the lines. And then command this. >> Jimmy is a power user. So that should be able to run and give us a solution. Okay, because we basically got rid of. So it's definitely got something to do with the elephant definition. >> Right. >> Right? So you can see that we’re getting the right kind of behavior, 3 here, 3 then, 3 and 3. So those all seem to be correct. So our problem is here. I don't see any error. Whoops. What's going on? Elephant at position t-1. I know it. There it is, we gotta take the position of t-1. All right. Right? We’ve got to look at what's happening now. Unsat still, dammit. [LAUGH] I thought we were there. We're looking at the wrong, all of this is t-1. Okay? So we're actually just looking at the wrong information when doing this calculation. >> Off by one at the time. >> All right now, that agrees so if we get rid of these, woah. >> Okay. >> We get the answer we expect, woah. There you go. So you’ve seen us make a very subtle error. Off by 1, very common. >> Yep. But we’ve solved it. There's the solution to the elephant problem. >> Yeah. >> And we’ve had to work hard. >> Yeah.