Tag: register
A farmer has to cross a river with wolf, goat, and cabbage without creating a situation where goat and wolf or goat and cabbage are at one bank of the river while the farmer is at the other one. You can find this online in multiple versions [MC][CTK].
The input IIN contains a parameter input that can take on the values farmer, wolf, goat, or cabbage, representing attempts to cross the river by respectively farmer alone, or farmer with wolf, goat, respectively cabbage. When an unsafe situation is created in which one item can eat another one, the output OEATEN() is generated, which returns to the initial state. When an invalid choice is made (an item is chosen that is at the wrong bank of the river), the output ONOK() is returned. When all items successfully crossed the river, the output ODONE() is generated.
We used the Uppaal [BDL04] GUI as an editor to create the extended finite state machine (EFSM) in Figure 1. By means of several Python scripts we automatically generated from the Uppaal .xml file a Java executable that represents the EFSM as a Java state machine and acts as SUT.
model.pdf Δ | 11K | February 14, 2015, at 07:44 PM |
model.register.xml Δ | 7K | February 14, 2015, at 07:44 PM |
model.svgz Δ | 7K | February 20, 2015, at 03:49 AM |
model.uppaal.xml Δ | 13K | February 14, 2015, at 07:44 PM |