workiong on testing repls

doc/examples/account2_expect.py

@@ -0,0 +1,14 @@
+import pexpect
+import sys
+
+def run(name,opts,res):
+    child = pexpect.spawn('./{}'.format(name))
+    child.logfile = sys.stdout
+    try:
+        child.expect('>')
+        child.sendline('account.withdraw(4)')
+        child.expect('account2.ivy: line 29: : assumption failed')
+        return True
+    except pexpect.EOF:
+        print child.before
+        return False

doc/examples/account3_expect.py

@@ -0,0 +1,25 @@
+import pexpect
+import sys
+
+def run(name,opts,res):
+    child = pexpect.spawn('./{}'.format(name))
+    child.logfile = sys.stdout
+    try:
+        child.expect('>')
+        child.sendline('account.deposit(5)')
+        child.expect('>')
+        child.sendline('ask_and_check_balance')
+        child.expect('ask')
+        child.expect(r'\?')
+        child.sendline('4')
+        child.expect('1')
+        child.expect('>')
+        child.sendline('ask_and_check_balance')
+        child.expect('ask')
+        child.expect(r'\?')
+        child.sendline('6')
+        child.expect('0')
+        return True
+    except pexpect.EOF:
+        print child.before
+        return False

doc/examples/account_expect.py

@@ -0,0 +1,29 @@
+import pexpect
+import sys
+
+def run(name,opts,res):
+    child = pexpect.spawn('./{}'.format(name))
+    child.logfile = sys.stdout
+    try:
+        child.expect('>')
+        child.sendline('account.get_balance')
+        child.expect('0')
+        child.expect('>')
+        child.sendline('account.deposit(5)')
+        child.expect('>')
+        child.sendline('account.get_balance')
+        child.expect('5')
+        child.expect('>')
+        child.sendline('account.withdraw(2)')
+        child.expect('>')
+        child.sendline('account.get_balance')
+        child.expect('3')
+        child.expect('>')
+        child.sendline('account.withdraw(4)')
+        child.expect('>')
+        child.sendline('account.get_balance')
+        child.expect('65535')
+        return True
+    except pexpect.EOF:
+        print child.before
+        return False

doc/examples/helloworld_expect.py

@@ -0,0 +1,14 @@
+import pexpect
+import sys
+
+def run(name,opts,res):
+    child = pexpect.spawn('./{}'.format(name))
+    child.logfile = sys.stdout
+    try:
+        child.expect('>')
+        child.sendline('hello')
+        child.expect('< world')
+        return True
+    except pexpect.EOF:
+        print child.before
+        return False

doc/examples/leader_election_ring_repl_err.ivy

@@ -0,0 +1,191 @@
+#lang ivy1.6
+
+################################################################################
+#
+# A module containing the axioms of total order
+#
+################################################################################
+
+module total_order_axioms(t) = {
+    relation (X:t < Y:t)
+    property [transitivity] X:t < Y & Y < Z -> X < Z
+    property [antisymmetry] ~(X:t < Y & Y < X)
+    property [totality] X:t < Y | X = Y | Y < X
+}
+
+################################################################################
+#
+# A module containing the injectivity axiom
+#
+################################################################################
+
+module injectivity_axioms(f) = {
+    axiom [injectivity] f(X) = f(Y) -> X = Y
+}
+
+################################################################################
+#
+# ADT describing a totally ordered datatype
+#
+################################################################################
+
+module total_order = {
+    type t
+    instantiate total_order_axioms(t)   # t is totally ordered
+}
+
+################################################################################
+#
+# ADT describing a ring topology.
+#
+# The module includes a ring_head and ring_tail elements, and a ring
+# total order relation.
+#
+# The module also includes get_next and get_prev actions.
+#
+# In this module, the ring topology is arbitrary and fixed.
+#
+################################################################################
+
+module ring_topology = {
+    type t
+
+    # Axioms that ensure that t is totally ordered with head the
+    # minimal element and tail the maximal element.
+
+    instantiate total_order_axioms(t)   # t is totally ordered
+
+    action get_next(x:t) returns (y:t)
+
+    object spec = {
+	after get_next {
+	    assert (y <= X & X <= x) | (x < y & ~ (x < Z & Z < y))
+	}
+    }
+}
+
+
+################################################################################
+#
+# Types, relations and functions describing state of the network
+#
+################################################################################
+
+# A totally ordered set of ids
+instance id : total_order
+
+# A ring topology of nodes
+instance node : ring_topology
+
+################################################################################
+#
+#  The assignments of id's to nodes
+#
+################################################################################
+
+object asgn = {
+
+    function pid(X:node.t) : id.t          # map each node to an id
+
+    axiom [injectivity] pid(X) = pid(Y) -> X = Y
+}
+
+
+################################################################################
+#
+# The transport-layer service specification
+#
+################################################################################
+
+object trans = {
+
+    relation sent(V:id.t, N:node.t) # The identity V is sent at node N
+    init ~sent(V, N)
+    
+    action send(dst:node.t, v:id.t)
+    action recv(dst:node.t, v:id.t)
+
+    object spec = {
+	before send {
+	    sent(v,dst) := true
+	}
+	before recv {
+	    assert sent(v,dst)
+	}
+    }
+}
+
+################################################################################
+#
+# The high-level service specification
+#
+################################################################################
+
+
+object serv = {
+
+    action elect(v:node.t)                 # called when v is elected leader
+
+    object spec = {
+	before elect {
+	    assert asgn.pid(v) >= asgn.pid(X)   # only the max pid can be elected
+	}
+    }
+}
+
+################################################################################
+#
+# The high-level protocol
+#
+################################################################################
+
+module process(pid) = {
+
+    action async(me:node.t) = {
+	call trans.send(node.get_next(me),pid(me))
+    }
+
+    implement trans.recv(me:node.t,v:id.t) {
+        if v = pid(me) {  # Found a leader
+            call serv.elect(me)
+        }
+	else if v > pid(me)  { # pass message to next node
+	    call trans.send(node.get_next(me),v)
+        }
+    }
+
+    conjecture ~(asgn.pid(N) < asgn.pid(P) & trans.sent(asgn.pid(N),N))
+    conjecture ~(asgn.pid(P) < asgn.pid(Q) & N:node.t < P & P < Q & trans.sent(asgn.pid(P),N))
+    conjecture ~(asgn.pid(N) < asgn.pid(P) & N < P & P < Q & trans.sent(asgn.pid(N),Q))
+    conjecture ~(asgn.pid(Q) < asgn.pid(N) & N < P & P < Q & trans.sent(asgn.pid(Q),P))
+
+}
+
+# instantiate one process per ring element
+
+instance app: process(asgn.pid)
+
+import serv.elect
+import trans.send
+export app.async
+export trans.recv
+
+isolate iso_app = app with node,id,trans,serv,asgn
+
+object node_impl = {
+    interpret node.t -> bv[1]
+    
+    implement node.get_next(x:node.t) returns (y:node.t) {
+	y := x + 1 
+   }
+}
+
+isolate iso_node = node, node_impl
+
+object id_impl = {
+    interpret id.t -> bv[1]
+}
+
+isolate iso_id = id, id_impl
+
+extract iso_impl = app,node_impl,id_impl

doc/examples/leader_election_ring_repl_err2.ivy

@@ -0,0 +1,191 @@
+#lang ivy1.6
+
+################################################################################
+#
+# A module containing the axioms of total order
+#
+################################################################################
+
+module total_order_axioms(t) = {
+    relation (X:t < Y:t)
+    property [transitivity] X:t < Y & Y < Z -> X < Z
+    property [antisymmetry] ~(X:t < Y & Y < X)
+    property [totality] X:t < Y | X = Y | Y < X
+}
+
+################################################################################
+#
+# A module containing the injectivity axiom
+#
+################################################################################
+
+module injectivity_axioms(f) = {
+    axiom [injectivity] f(X) = f(Y) -> X = Y
+}
+
+################################################################################
+#
+# ADT describing a totally ordered datatype
+#
+################################################################################
+
+module total_order = {
+    type t
+    instantiate total_order_axioms(t)   # t is totally ordered
+}
+
+################################################################################
+#
+# ADT describing a ring topology.
+#
+# The module includes a ring_head and ring_tail elements, and a ring
+# total order relation.
+#
+# The module also includes get_next and get_prev actions.
+#
+# In this module, the ring topology is arbitrary and fixed.
+#
+################################################################################
+
+module ring_topology = {
+    type t
+
+    # Axioms that ensure that t is totally ordered with head the
+    # minimal element and tail the maximal element.
+
+    instantiate total_order_axioms(t)   # t is totally ordered
+
+    action get_next(x:t) returns (y:t)
+
+    object spec = {
+	after get_next {
+	    assert (y <= X & X <= x) | (x < y & ~ (x < Z & Z < y))
+	}
+    }
+}
+
+
+################################################################################
+#
+# Types, relations and functions describing state of the network
+#
+################################################################################
+
+# A totally ordered set of ids
+instance id : total_order
+
+# A ring topology of nodes
+instance node : ring_topology
+
+################################################################################
+#
+#  The assignments of id's to nodes
+#
+################################################################################
+
+object asgn = {
+
+    function pid(X:node.t) : id.t          # map each node to an id
+
+    axiom [injectivity] pid(X) = pid(Y) -> X = Y
+}
+
+
+################################################################################
+#
+# The transport-layer service specification
+#
+################################################################################
+
+object trans = {
+
+    relation sent(V:id.t, N:node.t) # The identity V is sent at node N
+    init ~sent(V, N)
+    
+    action send(dst:node.t, v:id.t)
+    action recv(dst:node.t, v:id.t)
+
+    object spec = {
+	before send {
+	    sent(v,dst) := true
+	}
+	before recv {
+	    assert sent(v,dst)
+	}
+    }
+}
+
+################################################################################
+#
+# The high-level service specification
+#
+################################################################################
+
+
+object serv = {
+
+    action elect(v:node.t)                 # called when v is elected leader
+
+    object spec = {
+	before elect {
+	    assert asgn.pid(v) >= asgn.pid(X)   # only the max pid can be elected
+	}
+    }
+}
+
+################################################################################
+#
+# The high-level protocol
+#
+################################################################################
+
+module process(pid) = {
+
+    action async(me:node.t) = {
+	call trans.send(node.get_next(me),pid(me))
+    }
+
+    implement trans.recv(me:node.t,v:id.t) {
+        if v = pid(me) {  # Found a leader
+            call serv.elect(me)
+        }
+	else if v > pid(me)  { # pass message to next node
+	    call trans.send(node.get_next(me),v)
+        }
+    }
+
+    conjecture ~(asgn.pid(N) < asgn.pid(P) & trans.sent(asgn.pid(N),N))
+    conjecture ~(asgn.pid(P) < asgn.pid(Q) & N:node.t < P & P < Q & trans.sent(asgn.pid(P),N))
+    conjecture ~(asgn.pid(N) < asgn.pid(P) & N < P & P < Q & trans.sent(asgn.pid(N),Q))
+    conjecture ~(asgn.pid(Q) < asgn.pid(N) & N < P & P < Q & trans.sent(asgn.pid(Q),P))
+
+}
+
+# instantiate one process per ring element
+
+instance app: process(asgn.pid)
+
+import serv.elect
+import trans.send
+export app.async
+export trans.recv
+
+isolate iso_app = app with node,id,trans,serv,asgn
+
+object node_impl = {
+    interpret node.t -> bv[1]
+    
+    implement node.get_next(x:node.t) returns (y:node.t) {
+	y := x + 1 
+   }
+}
+
+isolate iso_node = node, node_impl
+
+object id_impl = {
+    interpret id.t -> bv[1]
+}
+
+isolate iso_id = id, id_impl
+
+extract iso_impl = app,id_impl,asgn

doc/examples/leader_election_ring_repl_expect.py

@@ -0,0 +1,23 @@
+import pexpect
+import sys
+
+def run(name,opts,res):
+    child = pexpect.spawn('./{}'.format(name))
+    child.logfile = sys.stdout
+    try:
+        child.expect('>')
+        child.sendline('app.async(0)')
+        child.expect(r'< trans.send\(1,1\)')
+        child.expect('>')
+        child.sendline('trans.recv(1,1)')
+        child.expect(r'trans.send\(0,1\)')
+        child.expect('>')
+        child.sendline('trans.recv(0,1)')
+        child.expect(r'serv.elect\(0\)')
+        child.expect('>')
+        child.sendline('trans.recv(0,0)')
+        child.expect(r'leader_election_ring_repl.ivy: line 113: : assumption failed')
+        return True
+    except pexpect.EOF:
+        print child.before
+        return False

doc/examples/leader_election_ring_repl_iso_impl_expect.py

@@ -0,0 +1,23 @@
+import pexpect
+import sys
+
+def run(name,opts,res):
+    child = pexpect.spawn('./{}'.format(name))
+    child.logfile = sys.stdout
+    try:
+        child.expect('>')
+        child.sendline('app.async(0)')
+        child.expect(r'< trans.send\(1,1\)')
+        child.expect('>')
+        child.sendline('trans.recv(1,1)')
+        child.expect(r'trans.send\(0,1\)')
+        child.expect('>')
+        child.sendline('trans.recv(0,1)')
+        child.expect(r'serv.elect\(0\)')
+        child.expect('>')
+        child.sendline('trans.recv(1,0)')
+        child.expect(r'serv.elect\(1\)')
+        return True
+    except pexpect.EOF:
+        print child.before
+        return False

ivy/ivy_to_cpp.py

@@ -24,7 +24,7 @@ import re
 
 def all_state_symbols():
     syms = il.all_symbols()
-    return [s for s in syms if s not in il.sig.constructors]
+    return [s for s in syms if s not in il.sig.constructors and slv.solver_name(il.normalize_symbol(s)) != None]
 
 def sort_card(sort):
     if hasattr(sort,'card'):

test/run_expects.py

@@ -1,6 +1,7 @@
 import pexpect
 import os
 import sys
+import imp
 
 checks = [
     ['../doc/examples/testing',
@@ -69,6 +70,28 @@ tests = [
      ]
 ]
 
+repls = [
+    ['../doc/examples',
+      [
+         ['leader_election_ring_repl','isolate=iso_impl','leader_election_ring_repl_iso_impl_expect'],
+#         ['helloworld',None],
+#         ['account',None],
+#         ['account2',None],
+#         ['account3',None],
+#         ['leader_election_ring_repl',None],
+      ]
+     ]
+]
+
+to_cpps = [
+    ['../doc/examples',
+      [
+         ['leader_election_ring_repl_err','target=repl','isolate=iso_impl','leader_election_ring_repl_err.ivy: line 90: error: relevant axiom asgn.injectivity not enforced'],
+#         ['leader_election_ring_repl_err2','target=repl','isolate=iso_impl','leader_election_ring_repl.ivy: error: No implementation for action node.get_next'],
+      ]
+     ]
+]
+
 
 class Test(object):
     def __init__(self,dir,args):
@@ -120,8 +143,15 @@ class IvyRepl(Test):
     def preprocess_commands(self):
         return ['ivy_to_cpp target=repl build=true '+' '.join(self.opts) + ' '+self.name+'.ivy']
     def expect(self):
-        pass
+        print 'wd:{}'.format(os.getcwd())
+        modname = self.res if self.res != None else (self.name+'_expect')
+        mod = imp.load_source(modname,modname+'.py')
+        return mod.run(self.name,self.opts,self.res)
     
+class IvyToCpp(Test):
+    def command(self):
+        return 'ivy_to_cpp ' + ' '.join(self.opts) + ' '+self.name+'.ivy'
+
 all_tests = []
 
 def get_tests(cls,arr):
@@ -130,9 +160,11 @@ def get_tests(cls,arr):
         for check in checkl:
             all_tests.append(cls(dir,check))
 
-get_tests(IvyCheck,checks)
+#get_tests(IvyCheck,checks)
 #get_tests(IvyTest,tests)
-        
+#get_tests(IvyRepl,repls)
+get_tests(IvyToCpp,to_cpps)
+
 num_failures = 0
 for test in all_tests:
     status = test.run()