Feature #158

Provide DFS search strategy for spec2lts-reach

Added by Anonymous about 11 years ago. Updated about 11 years ago.

Status:ClosedStart date:19 Aug 2009
Priority:LowDue date:
Assignee:Alfons Laarman% Done:

100%

Category:toolsEstimated time:16.00 hours
Target version:ltsmin-1.4Spent time:24.00 hours

Associated revisions

Revision 850b3834
Added by Michael Weber about 11 years ago

Refactored DFS and spec2lts-grey.c

  • made DFS strict (more book keeping)
  • added dfs/vset implementation
  • {dfs,bfs} x {tree,vset} all produce bisimilar LTSs
  • updated man page with new options
  • refactored state-buffer, dfs-stack
  • fixed size_t vs. int bug in dfs-stack.c
  • renamed state-buffer.[ch] to is-balloc.[ch]
TODO:
  • move TorX RPC into separate tool
  • test writing of state info; lack of means

(Closes #158)

Signed-off-by: Michael Weber <>

History

#1 Updated by Anonymous about 11 years ago

  • Estimated time changed from 16.00 to 24.00

#2 Updated by Anonymous about 11 years ago

  • Estimated time changed from 24.00 to 16.00

#3 Updated by Anonymous about 11 years ago

  • Status changed from Assigned to Resolved
  • % Done changed from 90 to 100

#4 Updated by Anonymous about 11 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF