Petrinets are used to analyse safety properties of a system, such as deadlock. Needless to say, the Petrinets resulting from your railway models will be abstractions. These abstractions need to be useful with respect to the properties you want to prove. For this exercise, you will have to prove, for a model with two trains, whether there is a way to schedule these trains fully independently. This means that they will, on their way from the start to the end station, never enter a segment that was entered by the other train. Knowing that two trains can run fully independently is useful, as a scheduler then would not need to worry about those two trains ever crashing. Make sure to fully explain in your report how your Petrinets representation can be used to prove this property.

Your transformation starts from a railway model with two trains and a simplified schedule: only the start and end stations for each train are known. This is because we don't want to constraint ourselves to one particular scheduling of the trains, we want to consider all of them. Encode your Petrinet in a way that allows to prove the property "the two trains can drive independently". This means that there for both trains, a path can be found from the start to end station that contains no segment the other train enters on its way from the start to end station. If one such pair of paths can be found, the property is proven.