maude-lang / Maude

Language based on Rewriting Logic
GNU General Public License v2.0
78 stars 10 forks source link

search for states with more than one successor #16

Closed dwightguth closed 8 months ago

dwightguth commented 9 months ago

Of interest to Runtime Verification is the ability to perform a search for states with more than one outbound arc. While we can simulate this functionality by performing a search of a particular depth and then examining and postprocessing the search graph that we get back, this has the undesirable property that it might perform more work than needed, potentially considerably more work. Thus, in the interests of performance, I propose a new search type to add to the search command in Maude. This search type searches for states with more than one successor in the same sense that the =>! search type searches for states with zero successors.

This is a draft of an attempt to add this functionality to Maude. It is provided in the interests of assisting in the final implementation of such a feature in Maude.