Example with PA-Match-All
Nevermind.
travis: enable travis-ci integration
travis: add build status badge to README
merge from main
refactor aspects of verify code into different files for equivalence/reachability split
rename NetCore -> NetKat for verify
Packets' previous-packet field now represents history
Print out dehopify time.
fix-semantics-size: Make size and size_pred tail recursive
Merge pull request #194 from frenetic-lang/fix-semantics-size

fix-semantics-size: Make size and size_pred tail recursive
Merge pull request #192 from frenetic-lang/travis

Travis-CI integration
switches: Group topology terms into switch terms

This commit changes the internal representation of topology terms within
the automaton-based dehopification algorithm. Previously, the algorithm
treated link terms in parallel composition as independent entities.

  topo = (1@1 => 2@1 | 1@2 => 3@1 | 2@1 => 3@2)

This meant that link-free policies would be distributed across the
entire parallel composition:

  lfp ; topo = (lfp ; 1@1 => 2@1) | (lfp ; 1@2 => 3@1) | ...

which would lead to rapid growth in transformed program size.

Instead, the algorithm now recognizes when link terms with the same
source switch are combined in parallel composition, and consider that a
single link term for the purposes of distributing sequences. The
distribution is actually done at a later point in the algorithm where it
can be implemented more efficiently as a port filter on the local
policy.

Note that this currently only applies for compositions that associate to
the left, which means you will only see the effect on one or two switch
policies if the policies are not crafted carefully. To clarify,

  (1@1 => 2@1 | 1@2 => 3@1 | 2@1 => 4@1 | 2@2 => 4@2)

will only group switch 1, whereas

  (1@1 => 2@1 | 1@2 => 3@1) | (2@1 => 4@1 | 2@2 => 4@2)

will group both switch 1 and switch 2.
switches: collect whole topolgy terms

This commit is a follow-up to the last, with further grouping of link
terms. Now, rather than just grouping links on the same switch, any
parallel composition of link terms is stored as a single unit. In other
orwds, the automaton now works over sequence of link-free policies and
topology terms.

Results: abfattree-tables-fail-full-4-3.kat

  Generate using the script in ocaml-topology:

    python abfattree.py -k abfattree-tables-fail-full-4-3.kat -t tables\
    -f fail -l full -o /tmp/f10.dot 4 3

  Running time:
    real    0m5.438s
    user    0m5.088s
    sys     0m0.036s

  Size of flowtables: 26 to 144

  Number of states used: 4 (including initial)

  Correctness: spot-checked but not confirmed.
switches: fix stack overflow in transformations

The transformations from a policy to a regex, as well as a link-free
policy to a policy, were not tail recursive and were therefore blowing
the stack on large in large inputs. This commit fixes that by CPS-ing
these functions, thus making them tail recursive.

Fixes #185
switches: elminiate redundant policy transformations

The code was distributing link-free policies across topology terms,
which meant that later on the copies of the link-free policies would
have to each copy would have to be transformed into a policy, thus
duplicating work. This commit transforms like-free polices into regular
policies before distributing across topology terms, thus elminating the
redundant work.
switches: use switchId type from SDN_Types

switchId is a type synonym for VInt.t, and so is reverse compatible.
switches: Fix Empty regex's corresponding policy

Empty matches the empty string, not any string. It corresponds to drop,
not id.
switch: preserve link-free policy in Star case

When converting a policy to a regex, in the case of a Star, there is no
need to wrap the result in a Kleene if it is a PChar. In that case, the
Star can be lowered into the PChar.
switches: add comments and TODOs