combining variations of a module

10 views
Skip to first unread message

Tim Leonard

unread,
Feb 12, 2021, 2:00:53 PM2/12/21
to tla...@googlegroups.com
I’ve written a module that specifies depth-first search over a directed graph. I now want to specify nested DFS, in which an inner DFS search is performed starting from each node reached by the outer DFS. Though the two searches will both do DFS, they will differ in having separate state variables, in having different initial values of those state variables, and in the predicate that recognizes a goal node if one is found. I don’t know how best to make those three things effectively be parameters of the module, or how best to modify the Next action so a module that incorporates both can properly sequence their respective executions. I’ve thought of a couple of different ways of doing it using the parts of TLA+ I’m familiar with, but thought it wisest to ask for advice rather than just forging ahead.

Reply all
Reply to author
Forward
0 new messages