Process FSM minimization for smaller CFSMs

[GoogleCodeExporter]

The conversion from GFSM to CFSM tends to produce CFSMs with process FSMs that 
have a high degree of redundancy (see example model in the attachment). This is 
not a correctness issue, but may impact:
(1) performance of the McScM model checker, and
(2) final model size that the user has to inspect.

This should be fixed by independently minimizing each of the process FSMs, 
possibly by using the dk.brics.automaton library.

Original issue reported on code.google.com by bestchai on 4 Oct 2012 at 1:57

Attachments:

• test.dot.2.png

[GoogleCodeExporter]

1. The process FSMs may be NFAs, therefore, to apply DFA minimization we must 
make sure that the FSM is a DFA.

2. Besides the (already implemented) merging of bisimular states, there is one 
more rule that would help to generate smaller NFAs:

Two states s1, and s2, can be merged if:
- there is a transition from s1 to s2 on e, and
- s1 has a self loop on e, and
- all transitions from s1 and s2 are equivalent (except for the self
loop on e), and
- set of transitions into s2 is a subset of the transitions into s2

This rule resembles the reverse of loop unrolling.

Original comment by bestchai on 5 Oct 2012 at 12:38

[GoogleCodeExporter]

Original comment by ssukkerd on 5 Nov 2012 at 11:04

• Changed state: Started

[GoogleCodeExporter]

Solution in revision 3f3542237dd6, please review.

Original comment by ssukkerd on 6 Nov 2012 at 9:24

[GoogleCodeExporter]

Merged into default in revision 3224fe3b74dd

Original comment by bestchai on 7 Nov 2012 at 12:10

• Changed state: Fixed