Open de onderstaande files in Uppaal:
Dit model beschrijft een eenvoudige werkplaats (een andere als staat beschreven in de handleiding!). We laten even in het midden wat hier precies gemaakt wordt, maar je zou kunnen denken aan een copyshop, een kledingsatelier, een fabriek voor motoronderdelen of een levensmiddelenbedrijf. Er zijn twee orders voor producten binnengekomen, Job1 en Job2. Om deze producten te maken zijn er drie machines beschikbaar, Machine1, Machine2 en Machine3. Voor order Job1 is eerst 2 uur Machine3 nodig, dan 2 uur Machine2 en tot slot 4 uur Machine1. Voor order Job2 is eerst 3 uur Machine3 nodig en dan 1 uur Machine3.In het model is er voor iedere machine een aparte automaat. Het basisidee is heel eenvoudig. Een MachineN begin als er een startN? transitie plaatsvindt. Een klok xN wordt dan op 0 gezet en gaat lopen. Wanneer klok xN de waarde tijdN heeft dan is de machine klaar en vindt er een transitie eindeN plaats. De machine wordt dus precies tijdN uur gebruikt. De variabele tijdN kan door een gebruiker ingesteld worden op het moment dat hij/zij de machine start.
Voor iedere order is er ook een aparte automaat. Om order Job1 uit te voeren starten we eerst Machine3 met een start3! transitie en geven daarbij aan dat we deze machine 2 uur nodig hebben (tijd3 := 2). Dan wachten we totdat Machine3 klaar is (einde3?). Vervolgens starten we Machine2 met een start2! transitie en geven aan dat we ook deze machine 2 uur nodig hebben (tijd2 := 2). We wachten tot Machine2 klaar is (einde2?) en starten dan tot slot Machine1 met een start1! transitie. Deze machine hebben we 4 uur nodig (tijd1 := 4). Wanneer Machine1 klaar is (einde1?) zijn we klaar met de order. De automaat voor Job2 ziet er soortgelijk uit.
Merk op dat in dit model iedere machine door hooguit één job tegelijk gebruikt kan worden. Aan het begin van de dag moeten we daarom een planning maken waarin we aangeven op welke tijden welke job gebruik mag maken van welke machine. Hieronder staat een mogelijke dagplanning waarbij in totaal 9 uur nodig is om de twee orders te verwerken.
E<> Job1.Klaar && Job2.Klaar && x <= 7vraag je Uppaal of er een planning is waarbij beide orders worden afgerond binnen 7 uur. Stel vast met behulp van Uppaal dat deze eigenschap niet geldt. Leg uit waarom het sowieso onmogelijk is om beide orders binnen 7 uur af te krijgen.