search

frenetic-lang / frenetic

The Frenetic Programming Language and Runtime System
http://www.frenetic-lang.org/
Other
223 stars 51 forks source link

NetKAT Decision Procedure Based on Symbolic Automata (FDDs) #558

Open smolkaj opened 7 years ago

smolkaj commented 7 years ago

Must:

Bugs:

May:

smolkaj commented 7 years ago

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

smolkaj commented 7 years ago

@jnfoster: Do we have examples from previous implementations?

jnfoster commented 7 years ago

Yes, we have the POPL '15 benchmarks.

m4lvin commented 6 years ago

Does this replace https://github.com/frenetic-lang/frenetic/pull/522? If I want a usable decision procedure, which branch should I use, verification_and_felix, equivalence or master?

jnfoster commented 6 years ago

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 commented 6 years ago

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

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 commented 6 years ago

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 notifications@github.com 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 https://github.com/frenetic-lang/frenetic/pull/558#issuecomment-377198564, or mute the thread https://github.com/notifications/unsubscribe-auth/ABwi0lvhXOXR81PBAoL0u-Jpl5gCt1CJks5tjL0PgaJpZM4M3Vxu .

m4lvin commented 6 years ago

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 commented 6 years ago

@m4lvin: I just pushed a commit (be47c929ed84904f9bdb81bf9765a0432db63069) 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 commented 6 years ago

@m4lvin: Also note that I had to make some changes to make things compile (587fe1a3c1b6bc8bfa2bd8f0defe1d615060ad35). 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 commented 6 years ago

Thank you @smolkaj! It compiles and runs :+1: 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 commented 6 years ago

Remind me, your example did not contain any dups, right? If so, i would expect a decent implementation to handle it almost instantly. On Mon, Apr 9, 2018 at 05:59 Malvin Gattinger notifications@github.com 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 https://github.com/frenetic-lang/frenetic/pull/558#issuecomment-379699848, or mute the thread https://github.com/notifications/unsubscribe-auth/AGVZcrx4l62heCmGPvII3AyoKDBiOMnGks5tmzD3gaJpZM4M3Vxu .

m4lvin commented 6 years ago

Correct, we do not use histories at all.

smolkaj commented 6 years ago

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 notifications@github.com 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 https://github.com/frenetic-lang/frenetic/pull/558#issuecomment-379768369, or mute the thread https://github.com/notifications/unsubscribe-auth/AGVZcnegKlJPU02TmM31fDVUXjDl5hlYks5tm23SgaJpZM4M3Vxu .