Skip to content
Permalink
Browse files

adding examples, notebooks

  • Loading branch information
kenmcmil committed Dec 28, 2015
1 parent 282a3a4 commit 6202b07e3755a3c7792a11db9fefea6247d1faa6
Showing with 13,267 additions and 0 deletions.
  1. +11 −0 INSTALL
  2. +11 −0 examples/examples.txt
  3. +115 −0 examples/ivy/abp.ivy
  4. +301 −0 examples/ivy/bakery.ivy
  5. +241 −0 examples/ivy/chord2s.ivy
  6. +241 −0 examples/ivy/chord2s_demo.ivy
  7. +251 −0 examples/ivy/chord2sbd.ivy
  8. +33 −0 examples/ivy/client_server.ivy
  9. +37 −0 examples/ivy/client_server_fp.ivy
  10. +39 −0 examples/ivy/client_server_sorted.ivy
  11. +537 −0 examples/ivy/flash.ivy
  12. +28 −0 examples/ivy/gc_abs.ivy
  13. +31 −0 examples/ivy/gc_abs2.ivy
  14. +240 −0 examples/ivy/gc_copy.ivy
  15. +302 −0 examples/ivy/gc_copy.save.ivy
  16. +305 −0 examples/ivy/gc_copy_oded.ivy
  17. +34 −0 examples/ivy/gc_temp_abs.ivy
  18. +240 −0 examples/ivy/gc_test.ivy
  19. +124 −0 examples/ivy/learning.ivy
  20. +132 −0 examples/ivy/learning_sorted_e.ivy
  21. +135 −0 examples/ivy/learning_sorted_non_epr.ivy
  22. +77 −0 examples/ivy/learning_switch.ivy
  23. +98 −0 examples/ivy/learning_un.ivy
  24. +125 −0 examples/ivy/learning_un_e.ivy
  25. +103 −0 examples/ivy/learning_un_ins.ivy
  26. +186 −0 examples/ivy/learning_with_count.ivy
  27. +177 −0 examples/ivy/learning_withcount.ivy
  28. +45 −0 examples/ivy/spanning_tree.ivy
  29. +284 −0 examples/ivy/tilelink1.ivy
  30. +623 −0 examples/ivy/tilelink2.ivy
  31. +452 −0 examples/ivy/tilelink_abstract_spec.ivy
  32. +24 −0 examples/ivy/tilelink_concrete_spec.ivy
  33. +600 −0 examples/ivy/tilelink_rcsc_snoopy.ivy
  34. +687 −0 examples/ivy/tilelink_rcsc_store_buffer.ivy
  35. +735 −0 examples/ivy/tilelink_rcsc_store_buffer2.ivy
  36. +735 −0 examples/ivy/tilelink_rcsc_store_buffer2_save.ivy
  37. +733 −0 examples/ivy/tilelink_rcsc_store_buffer2_temp.ivy
  38. +115 −0 examples/ivy/tilelink_snoopy.ivy
  39. +258 −0 examples/ivy/tilelink_store_buffer.ivy
  40. +71 −0 examples/ivy/tilelink_two_port_test_bench.ivy
  41. +219 −0 examples/pldi16/chain_panda3.ivy
  42. +226 −0 examples/pldi16/chain_panda4.ivy
  43. +289 −0 examples/pldi16/chord2s_cti.ivy
  44. +113 −0 examples/pldi16/learning_switch.ivy
  45. +202 −0 notebooks/Test.ipynb
  46. +169 −0 notebooks/bspline.ipynb
  47. +7 −0 notebooks/clear_outputs
  48. +481 −0 notebooks/client_server_demo.ipynb
  49. +493 −0 notebooks/client_server_demo_menus.ipynb
  50. +64 −0 notebooks/concept_graph.ipynb
  51. +102 −0 notebooks/flexboxes_bug.ipynb
  52. +177 −0 notebooks/hotel_with_ins.ivy.ipynb
  53. +236 −0 notebooks/iframes.ipynb
  54. +238 −0 notebooks/ivy12.ipynb
  55. +9 −0 notebooks/start_notebook_server
  56. +197 −0 notebooks/updr.ipynb
  57. +216 −0 notebooks/updr_leader.ipynb
  58. +313 −0 notebooks/updr_leader_dialogs.ipynb
11 INSTALL
@@ -0,0 +1,11 @@
Ivy needs:

python 2.7
IPython 3.2
ply (python lex yacc)
Z3 python interface (import z3 should work)
pygraphviz 1.3.1 (which requires graphviz)

symbolic link (linux) or directory junction (windows) from ~/.ipython/nbextensions/ivy to ivy2/ivy

On windows, the best way to get IPython and ply is to install Anaconda: http://continuum.io/downloads
@@ -0,0 +1,11 @@
learning - proved, using updr
learning with count
spanning tree
leader - proved, using iupdr
client server
chord
flash
hotel
chain panda
gc copy - proved, mainly using cti
bakery
@@ -0,0 +1,115 @@
#lang ivy1.2

type bit = {zero,one}

type univ

module intf(sndr,rcvr) = {

individual state : bit
relation pending

init state = one & ~pending

action put(v : bit) = {
assert ~pending & v ~= state;
state := v;
pending := true
}
mixin put before rcvr:put

action get(v : bit) = {
assert pending & v = state;
pending := false
}
mixin get before sndr:get
}

module channel(sndr,rcvr) = {
individual state : bit
relation put_pending
relation get_pending

init ~put_pending & ~get_pending & state = one

action get(v : bit) = {
get_pending := true;
state := v
}

action put(v : bit) = {
put_pending := true;
state := v
}

action step = {
if * {
assume get_pending;
get_pending := false;
call sndr:get(state)
}
else {
assume put_pending;
put_pending := false;
call rcvr:put(state)
}
}
}

module sender(rcvr) = {

individual state : bit
relation pending

init ~pending & state = one

action get(v : bit) = {
pending := false
}

action step(v : bit) = {
assume ~pending;
assume v ~= state;
pending := true;
state := v;
call rcvr:put(v)
}

}

module receiver(sndr) = {

individual state : bit
relation pending

init ~pending

action put(v : bit) = {
pending := true;
state := v
}

action step = {
assume pending;
# call sndr:get(state);
call sndr:get(zero);
pending := false
}

}

instantiate s : sender(c)
instantiate c : channel(s,r)
instantiate r : receiver(c)

export s:step
export c:step
export r:step

instantiate sc : intf(s,c)
instantiate sr : intf(c,r)

isolate iso_s = s with sc
isolate iso_c = c with sc,sr
isolate iso_r = r with sr

0 comments on commit 6202b07

Please sign in to comment.
You can’t perform that action at this time.