search

ssomayyajula / equiv

Equivalence in NetKAT modulo specifications
1 stars 0 forks source link

`Expand` functor broken #1

Open ssomayyajula opened 7 years ago

ssomayyajula commented 7 years ago

The defined continuation and observation maps in the Expand functor in Frenetic_Decide_FA don't properly enumerate packets in the same ENUM so it only works on alpha F selectors.

ssomayyajula commented 7 years ago

We'll probably have to figure out an isomorphism between size-bounded finite sets over ENUMerated types with strictly positive integers so that they too can be considered an ENUM. Then, the simulation check should be done on the non-expanded automata.