Tim Leonard
unread,Feb 12, 2021, 2:00:53 PM2/12/21Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Sign in to report message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
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.