[tlaplus] combining variations of a module

[Tim Leonard <Tim@xxxxxxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/EE30F47D-A11C-4581-AB7C-FE4ED58DA3D3%40RyanLeonard.us.