Predicates over the Transportation Net Domain. We refer to Appendix A, Sect. A.l, Transportation Net. We also refer to Example 9.12 in which we suggested some types, some observer functions, and an axiom covering two constraints. But those constraints were not enough to satisfy suitably well-formed transportation nets. (i) If from any segment one can observe some connections, then from each of these connections one should be able to observe (at least) that segment. And: (ii) If from any connection one can observe some segments, then from each of these segments one should be able to observe (at least) that connection.
1. Formulate suitable axioms (i.e., a predicate expressions) expressing these two constraints.
2. Can you think of other constraints?
3. We wish to insert in a given transportation net a new segment, and assume that it is to be connected to existing connections. State the signature of a suitable insert_segment function, and state the pre- and post-conditions for this function.
4. We wish to insert in a given transportation net a new connection, and assume that it is to be inserted in an existing segment. State the signature of a suitable insert-connection function, and state the pre- and post-conditions for this function.