top relation TransitionToTransition {
		label:String;
		sourceTPN:pn::Place{};
		destTPN:pn::Place{};
		checkonly domain fsm t:fsm::Transition {
			input=label,
			from=sourceTFSM:fsm::State{},
			to=destTFSM:fsm::State{},
			fsm=f:fsm::FSM{}
		};
		enforce domain petri p:pn::Transition {
			input=label,
			from=sourceTPN,
			to=destTPN,
			 net=pn:pn::PetriNet{}
		};
		when {
			AutomataToNet(f,pn);
			StateToPlace(sourceTFSM,sourceTPN);
			StateToPlace(destTFSM,destTPN);
		}
	}