added attributes method and separate

ivy/ivy_check.py

@@ -26,7 +26,7 @@ coverage = iu.BooleanParameter("coverage",True)
 checked_action = iu.Parameter("action","")
 opt_trusted = iu.BooleanParameter("trusted",False)
 opt_mc = iu.BooleanParameter("mc",False)
-opt_separate = iu.BooleanParameter("separate",False)
+opt_separate = iu.BooleanParameter("separate",None)
 
 def display_cex(msg,ag):
     if diagnose.get():
@@ -455,9 +455,22 @@ def all_assert_linenos():
         raise iu.IvyError(None,'There is no assertion at the specified line')
     return res
 
-def mc_isolate():
+def get_isolate_attr(isolate,attr,default=None):
+    attr = iu.compose_names(isolate,attr)
+    if attr not in im.module.attributes:
+        return default
+    return im.module.attributes[attr].rep
+
+def check_separately(isolate):
+    if opt_separate.get() is not None:
+        return opt_separate.get()
+    return get_isolate_attr(isolate,'separate','false') == 'true'
+
+def mc_isolate(isolate):
+    if im.module.labeled_props:
+        raise IvyError(im.module.labeled_props[0],'model checking not supported for property yet')
     import ivy_mc
-    if not opt_separate.get():
+    if not check_separately(isolate):
         with im.module.theory_context():
             ivy_mc.check_isolate()
         return
@@ -469,6 +482,11 @@ def mc_isolate():
                 ivy_mc.check_isolate()
             act.checked_assert.value = old_checked_assert
     
+def get_isolate_method(isolate):
+    if opt_mc.get():
+        return 'mc'
+    return get_isolate_attr(isolate,'method','ic')
+
 
 def check_module():
     # If user specifies an isolate, check it. Else, if any isolates
@@ -501,8 +519,8 @@ def check_module():
             ivy_isolate.create_isolate(isolate) # ,ext='ext'
             if opt_trusted.get():
                 continue
-            if opt_mc.get():
-                mc_isolate()
+            if get_isolate_method(isolate) == 'mc':
+                mc_isolate(isolate)
             else:
                 check_isolate()
     print ''

ivy/ivy_compiler.py

@@ -754,7 +754,7 @@ def resolve_alias(name):
         return resolve_alias(parts[0]) + iu.ivy_compose_character + parts[1]
     return name
 
-defined_attributes = set(["weight","test"])
+defined_attributes = set(["weight","test","method","separate"])
 
 class IvyDomainSetup(IvyDeclInterp):
     def __init__(self,domain):
@@ -1061,7 +1061,7 @@ class IvyARGSetup(IvyDeclInterp):
         oname = iu.ivy_compose_character.join(fields[:-1])
         oname = 'this' if oname == '' else oname
         aname = fields[-1]
-        if oname not in self.mod.actions and oname not in self.mod.hierarchy:
+        if oname != 'this' and oname not in self.mod.actions and oname not in self.mod.hierarchy:
             raise IvyError(a,'"{}" does not name an action or object'.format(oname))
         if aname not in defined_attributes:
             raise IvyError(a,'"{}" does not name a defined attribute'.format(aname))

ivy/ivy_lexer.py

@@ -245,7 +245,7 @@ class LexerVersion(object):
                 if s in reserved:
                     del reserved[s]
         else:
-            for s in ['requires','ensures']:
+            for s in ['requires','ensures','method']:
                 if s in reserved:
                     del reserved[s]
 

ivy/ivy_mc.py

@@ -14,6 +14,7 @@ import tempfile
 import subprocess
 from collections import defaultdict
 import itertools
+import sys
 
 logfile = None
 
@@ -1426,7 +1427,7 @@ def check_isolate():
     texts = []
     while True:
         text = p.stdout.read(256)
-        print text,
+        sys.stdout.write(text)
         texts.append(text)
         if len(text) < 256:
             break

ivy/ivy_parser.py

@@ -1385,8 +1385,22 @@ def p_top_nativequote(p):
     thing.lineno = get_lineno(p,2)
     p[0].declare(thing)   
 
-def p_top_attribute_callatom_eq_callatom(p):
-    'top : top ATTRIBUTE callatom EQ callatom'
+def p_top_attributeval_callatom(p):
+    'attributeval : callatom'
+    p[0] = p[1]
+
+def p_top_attributeval_true(p):
+    'attributeval : TRUE'
+    p[0] = Atom('true')
+    p[0].lineno = get_lineno(p,1)
+
+def p_top_attributeval_false(p):
+    'attributeval : FALSE'
+    p[0] = Atom('false')
+    p[0].lineno = get_lineno(p,1)
+
+def p_top_attribute_callatom_eq_attributeval(p):
+    'top : top ATTRIBUTE callatom EQ attributeval'
     p[0] = p[1]
     defn = AttributeDef(p[3],p[5])
     defn.lineno = get_lineno(p,2)

test/flash2_mc.ivy

@@ -514,67 +514,4 @@ proof let H = home
 
 include mc_schemata
 
-# schema trans1 = {
-#     type t
-#     function x : t
-#     function z : t
-#     property x = X & z = X -> x = z
-# }
-
-# schema trans2 = {
-#     type t
-#     function x : t
-#     property Y = X  -> (x = X <-> x = Y)
-# }
-
-# schema contra = {
-#     type t
-#     function x : t
-#     property Y ~= X -> ~(x = X & x = Y)
-# }
-
-# # schema cong1 = {
-# #     type t
-# #     type u
-# #     function x : t
-# #     function f1(X:t) : u
-# #     property x = X -> f1(x) = f1(X)
-# # }
-
-# schema cong1 = {
-#     type t
-#     type u
-#     function x : t
-#     function y : u
-#     function f1(X:t) : u
-#     property (f1(X) = y <-> f1(x) = y) | x ~= X 
-# }
-
-# schema cong1b = {
-#     type t
-#     type u
-#     function x : t
-#     function f2(X:t) : u
-#     property (f2(X) = f2(x)) | x ~= X 
-# }
-
-# schema cong2 = {
-#     type t1
-#     type t2
-#     type u
-#     function x1 : t1
-#     function x2 : t2
-#     function y : u
-#     function f1(X1:t1,X2:t2) : u
-#     property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
-# }
-
-# schema cong2b = {
-#     type t1
-#     type t2
-#     type u
-#     function x1 : t1
-#     function x2 : t2
-#     function f1(X1:t1,X2:t2) : u
-#     property (f1(X1,X2) = f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
-# }
+attribute method = mc

test/ibm-cache-N_mc.ivy

@@ -127,3 +127,5 @@ export receiveinvalidateAckRule
 export grantexclusiveRule
 export receivesharedGrantRule
 export grantsharedRule
+
+attribute method = mc

test/toma8_mc.ivy

@@ -286,3 +286,4 @@ export toma.step
 
 include mc_schemata
 
+attribute method = mc

test/vsync_paxos.ivy

@@ -278,3 +278,6 @@ export decide
 
 include mc_schemata
 instantiate total_order_schemata(stake)
+
+attribute method = mc
+attribute separate = true