For a project I have in mind, I’m trying to investigate if Coq could suit my need.
I’m trying to model a data flow diagram. In a data flow diagram, I have assets that can be either processes, or data stores, or data flows.
Data flows can only be between two processes, or between a process and a data store. It is not correct to specify a data flow between to 2 data stores, or if at least one of the assets is a data flow itself.
I could do something like this:
Inductive Asset : Type :=
| DataFlow (a b : Asset).
But this is not correct enough for me, because at allows incorrect combinations of Asset to build a DataFlow.
How can I constrain my DataFlow constructor to only accept a pair of (Process, Process), or (Process, DataStore) or (DataStore, Process) ?
Or maybe, suggestions to do it completely differently ?
Thanks in advance.