The situation calculus logic model is most convenient for modelling the actions that can occur in an information system application. The interplay of pre-conditions and post-conditions not only determines a semantically justified partial order of the defined actions, but also serves to enforce integrity constraints. This form of specification allows the use of plan-generation algorithms to investigate, before the system is liberated for official usage, whether the proposed specification allows all desirable use cases, and effectively disallows the illegal or, for some reason, undesirable ones. On the other hand, especially for legacy applications, implemented without a prior specification, Process Mining techniques have been employed to derive an implicit Petri net model from the analysis of a large enough number of traces registered in an execution log. However, as a system just begins to be used, with a still empty execution log, this sort of process mining discovery would not be feasible. We shall explain in this paper how the Petri net model can be directly derived from the situation calculus specification rules. The main gist of the present research is to provide evidence that the two models are complementary, not only because the Petri net model is derivable from the situation calculus model, but also in view of the distinct advantages of the two models. While the situation calculus model leads to planning and simulated execution prior to implementation, the Petri net model, like other workflow engines, can be designed to run in a tightly restrictive mode, with the additional asset of intuitive visualization of the workable sequences. As proof of concept, we developed a prototype to demonstrate our methods, and tried it on two example cases: 1. a published request processing application used to introduce process mining notions, and 2. an analogously structured trial by combat application taken from a popular movie. The prototype includes an interactive dramatization component, which serves -as a mandatory requirement for digital entertainment pieces -to enact the second application.