NetKAT Decision Procedure Based on Symbolic Automata (FDDs)

[smolkaj]

Must:

• need more examples
• add documentation
• unit tests

Bugs:

• must not ignore inequality constraints

May:

• generate (minimal?) counterexamples
• verify automata manipulations?

[smolkaj]

Could it be that I implemented a correct decision procedure on first attempt?
I suppose we need more tests cases...

[smolkaj]

@jnfoster: Do we have examples from previous implementations?

[jnfoster]

Yes, we have the POPL '15 benchmarks.

[m4lvin]

Does this replace #522? If I want a usable decision procedure, which branch should I use, verification_and_felix, equivalence or master?

[jnfoster]

I would use Verification and Felix for the time being. Sorry for the confusion. We are working on getting the changes upstreamed to master with a new group of students.

[m4lvin]

Thanks! We got the verification_and_felix branch running and the decide command works for small examples of what we are trying to do 😃

Unfortunately, the shell or the parser seem to be limited to 4096 characters. I guess we should properly use your library instead of the shell? What is the best way to run the decide command on longer inputs? Can we somehow import text files and then use them in decide?

[jnfoster]

Can you send us a scenario to look at? The parser should handle very large inputs.

…

-N

On Thu, Mar 29, 2018 at 6:53 AM, Malvin Gattinger ***@***.***> wrote: Thanks! We got the verification_and_felix branch running and the decide command works for small examples of what we are trying to do 😃 Unfortunately, the shell or the parser seem to be limited to 4096 characters. I guess we should properly use your library instead of the shell? What is the best way to run the decide command on longer inputs? Can we somehow import text files and then use them in decide? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#558 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABwi0lvhXOXR81PBAoL0u-Jpl5gCt1CJks5tjL0PgaJpZM4M3Vxu> .

[m4lvin]

Here is a full example, please tell me if you need further details.

$ git branch
  master
* verification_and_felix
$ ./frenetic.native version
RWO
5.0
$ ./frenetic.native shell
Frenetic Shell v 4.0
Type `help` for a list of commands
frenetic> decide ((ag=0;pt=1;Saa=1;Sab=0;Naa=1;Nab=1;Sba=0;Sbb=1;Nba=0;Nbb=1);(((ag:=0;pt:=1)+(ag:=1;pt:=3));((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0))))+(ag=1;pt=3;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0))))))*;((Nab=0+Sab=1);(Nba=0+Sba=1))) == ((ag=0;pt=1;Saa=1;Sab=0;Naa=1;Nab=1;Sba=0;Sbb=1;Nba=0;Nbb=1);(((ag:=0;pt:=1)+(ag:=1;pt:=3));((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0))))+(ag=1;pt=3;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0))))))*;((Saa=1;Sab=1);(Sba=1;Sbb=1)))                                                             
true
frenetic> decide ((ag=0;pt=1;Saa=1;Sab=0;Naa=1;Nab=0;Sba=0;Sbb=1;Nba=0;Nbb=1);(((ag:=0;pt:=1)+(ag:=1;pt:=3));((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0))))+(ag=1;pt=3;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0))))))*;((Nab=0+Sab=1);(Nba=0+Sba=1))) == ((ag=0;pt=1;Saa=1;Sab=0;Naa=1;Nab=0;Sba=0;Sbb=1;Nba=0;Nbb=1);(((ag:=0;pt:=1)+(ag:=1;pt:=3));((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0))))+(ag=1;pt=3;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0))))))*;((Saa=1;Sab=1);(Sba=1;Sbb=1)))                                                             
false
frenetic> decide ((ag=0;pt=1;Saa=1;Sab=0;Sac=0;Naa=1;Nab=1;Nac=0;Sba=0;Sbb=1;Sbc=0;Nba=0;Nbb=1;Nbc=1;Sca=0;Scb=0;Scc=1;Nca=0;Ncb=0;Ncc=1);(((ag:=0;pt:=1)+(ag:=1;pt:=4)+(ag:=2;pt:=7));(((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0));(((Sac=1;Sbc:=1)+Sac=0);((Sbc=1;Sac:=1)+Sbc=0);((Nac=1;Nbc:=1)+Nac=0);((Nbc=1;Nac:=1)+Nbc=0))))+(ag=0;pt=1;Sac=0;Nac=1;((((Saa=1;Sca:=1)+Saa=0);((Sca=1;Saa:=1)+Sca=0);((Naa=1;Nca:=1)+Naa=0);((Nca=1;Naa:=1)+Nca=0));(((Sab=1;Scb:=1)+Sab=0);((Scb=1;Sab:=1)+Scb=0);((Nab=1;Ncb:=1)+Nab=0);((Ncb=1;Nab:=1)+Ncb=0));(((Sac=1;Scc:=1)+Sac=0);((Scc=1;Sac:=1)+Scc=0);((Nac=1;Ncc:=1)+Nac=0);((Ncc=1;Nac:=1)+Ncc=0)))))+(((ag=1;pt=4;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0));(((Sbc=1;Sac:=1)+Sbc=0);((Sac=1;Sbc:=1)+Sac=0);((Nbc=1;Nac:=1)+Nbc=0);((Nac=1;Nbc:=1)+Nac=0))))+(ag=1;pt=4;Sbc=0;Nbc=1;((((Sba=1;Sca:=1)+Sba=0);((Sca=1;Sba:=1)+Sca=0);((Nba=1;Nca:=1)+Nba=0);((Nca=1;Nba:=1)+Nca=0));(((Sbb=1;Scb:=1)+Sbb=0);((Scb=1;Sbb:=1)+Scb=0);((Nbb=1;Ncb:=1)+Nbb=0);((Ncb=1;Nbb:=1)+Ncb=0));(((Sbc=1;Scc:=1)+Sbc=0);((Scc=1;Sbc:=1)+Scc=0);((Nbc=1;Ncc:=1)+Nbc=0);((Ncc=1;Nbc:=1)+Ncc=0)))))+((ag=2;pt=7;Sca=0;Nca=1;((((Sca=1;Saa:=1)+Sca=0);((Saa=1;Sca:=1)+Saa=0);((Nca=1;Naa:=1)+Nca=0);((Naa=1;Nca:=1)+Naa=0));(((Scb=1;Sab:=1)+Scb=0);((Sab=1;Scb:=1)+Sab=0);((Ncb=1;Nab:=1)+Ncb=0);((Nab=1;Ncb:=1)+Nab=0));(((Scc=1;Sac:=1)+Scc=0);((Sac=1;Scc:=1)+Sac=0);((Ncc=1;Nac:=1)+Ncc=0);((Nac=1;Ncc:=1)+Nac=0))))+(ag=2;pt=7;Scb=0;Ncb=1;((((Sca=1;Sba:=1)+Sca=0);((Sba=1;Sca:=1)+Sba=0);((Nca=1;Nba:=1)+Nca=0);((Nba=1;Nca:=1)+Nba=0));(((Scb=1;Sbb:=1)+Scb=0);((Sbb=1;Scb:=1)+Sbb=0);((Ncb=1;Nbb:=1)+Ncb=0);((Nbb=1;Ncb:=1)+Nbb=0));(((Scc=1;Sbc:=1)+Scc=0);((Sbc=1;Scc:=1)+Sbc=0);((Ncc=1;Nbc:=1)+Ncc=0);((Nbc=1;Ncc:=1)+Nbc=0))))))))*;((Nab=0+Sab=1);(Nac=0+Sac=1);(Nba=0+Sba=1);(Nbc=0+Sbc=1);(Nca=0+Sca=1);(Ncb=0+Scb=1))) == ((ag=0;pt=1;Saa=1;Sab=0;Sac=0;Naa=1;Nab=1;Nac=0;Sba=0;Sbb=1;Sbc=0;Nba=0;Nbb=1;Nbc=1;Sca=0;Scb=0;Scc=1;Nca=0;Ncb=0;Ncc=1);(((ag:=0;pt:=1)+(ag:=1;pt:=4)+(ag:=2;pt:=7));(((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0));(((Sac=1;Sbc:=1)+Sac=0);((Sbc=1;Sac:=1)+Sbc=0);((Nac=1;Nbc:=1)+Nac=0);((Nbc=1;Nac:=1)+Nbc=0))))+(ag=0;pt=1;Sac=0;Nac=1;((((Saa=1;Sca:=1)+Saa=0);((Sca=1;Saa:=1)+Sca=0);((Naa=1;Nca:=1)+Naa=0);((Nca=1;Naa:=1)+Nca=0));(((Sab=1;Scb:=1)+Sab=0);((Scb=1;Sab:=1)+Scb=0);((Nab=1;Ncb:=1)+Nab=0);((Ncb=1;Nab:=1)+Ncb=0));(((Sac=1;Scc:=1)+Sac=0);((Scc=1;Sac:=1)+Scc=0);((Nac=1;Ncc:=1)+Nac=0);((Ncc=1;Nac:=1)+Ncc=0)))))+(((ag=1;pt=4;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0));(((Sbc=1;Sac:=1)+Sbc=0);((Sac=1;Sbc:=1)+Sac=0);((Nbc=1;Nac:=1)+Nbc=0);((Nac=1;Nbc:=1)+Nac=0))))+(ag=1;pt=4;Sbc=0;Nbc=1;((((Sba=1;Sca:=1)+Sba=0);((Sca=1;Sba:=1)+Sca=0);((Nba=1;Nca:=1)+Nba=0);((Nca=1;Nba:=1)+Nca=0));(((Sbb=1;Scb:=1)+Sbb=0);((Scb=1;Sbb:=1)+Scb=0);((Nbb=1;Ncb:=1)+Nbb=0);((Ncb=1;Nbb:=1)+Ncb=0));(((Sbc=1;Scc:=1)+Sbc=0);((Scc=1;Sbc:=1)+Scc=0);((Nbc=1;Ncc:=1)+Nbc=0);((Ncc=1;Nbc:=1)+Ncc=0)))))+((ag=2;pt=7;Sca=0;Nca=1;((((Sca=1;Saa:=1)+Sca=0);((Saa=1;Sca:=1)+Saa=0);((Nca=1;Naa:=1)+Nca=0);((Naa=1;Nca:=1)+Naa=0));(((Scb=1;Sab:=1)+Scb=0);((Sab=1;Scb:=1)+Sab=0);((Ncb=1;Nab:=1)+Ncb=0);((Nab=1;Ncb:=1)+Nab=0));(((Scc=1;Sac:=1)+Scc=0);((Sac=1;Scc:=1)+Sac=0);((Ncc=1;Nac:=1)+Ncc=0);((Nac=1;Ncc:=1)+Nac=0))))+(ag=2;pt=7;Scb=0;Ncb=1;((((Sca=1;Sba:=1)+Sca=0);((Sba=1;Sca:=1)+Sba=0);((Nca=1;Nba:=1)+Nca=0);((Nba=1;Nca:=1)+Nba=0));(((Scb=1;Sbb:=1)+Scb=0);((Sbb=1;Scb:=1)+Sbb=0);((Ncb=1;Nbb:=1)+Ncb=0);((Nbb=1;Ncb:=1)+Nbb=0));(((Scc=1;Sbc:=1)+Scc=0);((Sbc=1;Scc:=1)+Sbc=0);((Ncc=1;Nbc:=1)+Ncc=0);((Nbc=1;Ncc:=1)+Nbc=0))))))))*;((Saa=1;Sab=1;Sac=1);(Sba=1;Sbb=1;Sbc=1);(Sca=1;Scb=1;Scc=1)))
Parse error :14088:

I think that in the error :14088 should actually be 1:4088 meaning line 1, column 4088. And 4088 is roughly 4096 minus the length of "decide ", so this made us think that the parser or maybe the shell library has a limit at 2^12.
(How) can I load a NetKAT policy from a text file into the frenetic shell and then run decide on it?

(cc @janawagemaker)

[smolkaj]

@m4lvin: I just pushed a commit (be47c92) that adds a frenetic decide command:

$pwd
/home/steffen/src/frenetic-lang/frenetic/examples/decision-procedure

$ frenetic decide \#558-1.kat 
true

$ frenetic decide \#558-2.kat 
false

$ frenetic decide \#558-3.kat 
^C

This should fix the problem, also it looks like this implementation of the decision procedure doesn't scale well....

[smolkaj]

@m4lvin: Also note that I had to make some changes to make things compile (587fe1a). You should be able to build the branch with ocaml 4.03.0 by running the following:

# switch to the right version of ocaml
opam switch 4.03.0
eval `opam config env`

# install necessary dependencies
opam pin add frenetic . -n
opam install --deps-only frenetic

# build
make

[m4lvin]

Thank you @smolkaj! It compiles and runs 👍 The "decide" command was exactly what we needed.

Our third example still runs forever, though. Is the new procedure based on FDDs faster? Please let me know once it is usable and we'll switch to this branch here.

[smolkaj]

Remind me, your example did not contain any `dup`s, right? If so, i would expect a decent implementation to handle it almost instantly.

…

On Mon, Apr 9, 2018 at 05:59 Malvin Gattinger ***@***.***> wrote: Thank you @smolkaj <https://github.com/smolkaj>! It compiles and runs 👍 The "decide" command was exactly what we needed. Our third example still runs forever, though. Is the new procedure based on FDDs faster? Please let me know once it is usable and we'll switch to this branch here. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#558 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AGVZcrx4l62heCmGPvII3AyoKDBiOMnGks5tmzD3gaJpZM4M3Vxu> .

[m4lvin]

Correct, we do not use histories at all.

[smolkaj]

Yeah, the history-free fragment is easy to decide. (1) Compile the two programs to FDDs (2) Check equivalence of the FDD Step (2) is linear in the size of the FDDs. For step (1), we have a fast compiler that should scale very far.

…

On Mon, Apr 9, 2018 at 10:19 Malvin Gattinger ***@***.***> wrote: Correct, we do not us histories at all. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#558 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AGVZcnegKlJPU02TmM31fDVUXjDl5hlYks5tm23SgaJpZM4M3Vxu> .