import intrepid as ip
import intrepid.utils
import A7E_requirements
import time
import sys

def mk_negation_of_property_3(ctx, inst):
    navigationUpdateMode = inst.nets['A7E_requirements/NU/Mode']
    weaponDeliveryMode = inst.nets['A7E_requirements/WD/Mode']
    aflyUpdate = inst.nets['A7E_requirements/NU/AflyUpd']
    boc = inst.nets['A7E_requirements/WD/BOC']
    sboc = inst.nets['A7E_requirements/WD/SBOC']
    pre = ip.mk_eq(ctx, navigationUpdateMode, aflyUpdate)
    post1 = ip.mk_neq(ctx, weaponDeliveryMode, boc)
    post2 = ip.mk_neq(ctx, weaponDeliveryMode, sboc)
    post = ip.mk_and(ctx, post1, post2)
    # NavUpd=AflyUpd /\ WpnDel!=BOC /\ WpnDel!=SBOC
    target = ip.mk_and(ctx, pre, post)
    return target

if __name__ == "__main__":
    startTime = time.time()
    ctx = ip.mk_ctx()
    inst = A7E_requirements.SimulinkCircuit(ctx, 'A7E')
    inst.mk_circuit()
    wdm = inst.nets['A7E_requirements/WD/Mode']
    num = inst.nets['A7E_requirements/NU/Mode']
    prsTime = time.time() - startTime
    negProp3 = mk_negation_of_property_3(ctx, inst) 

    br = ip.mk_engine_br(ctx)
    ip.br_add_target(ctx, br, negProp3)
    ip.br_add_watch(ctx, br, negProp3)
    result = ip.br_reach_targets(br)
    print "Unreachable: ", result == ip.INT_ENGINE_RESULT_UNREACHABLE

    # bmc = ip.mk_engine_bmc(ctx)
    # wdmfs = inst.nets['A7E_requirements/WDMFS']
    # ow = inst.nets['A7E_requirements/Other_Weapon']
    # wmboc = inst.nets['A7E_requirements/ro19'] 
    # ip.bmc_add_watch(ctx, bmc, wdmfs)
    # ip.bmc_add_watch(ctx, bmc, ow)
    # ip.bmc_add_watch(ctx, bmc, wmboc)
    # ip.bmc_add_target(ctx, bmc, negProp3)
    # for depth in range(0, 50):
    #     print "Trying depth", depth
    #     ip.set_bmc_current_depth(bmc, depth)
    #     result = ip.bmc_reach_targets(bmc)
    #     if result == ip.INT_ENGINE_RESULT_REACHABLE:
    #         print "Reachable"
    #         cex = ip.bmc_get_counterexample(ctx, bmc, negProp3)
    #         cexDict = ip.utils.counterexample_get_as_dictionary(ctx, cex, inst.inputs, { 'NUM' : num,\
    #         										 'WDM' : wdm,\
    #     										 'WDMFS' : wdmfs,\
    #     										 'OthWp' : ow,\
    #     										 'WM=BOC' : wmboc })
    #         cexDf = ip.utils.counterexample_get_as_dataframe(cexDict)
    #         print cexDf
    #         break
    #     sys.stdout.flush()
    # ip.del_ctx(ctx)

    endTime = time.time() - startTime
    print 'Parse time:', prsTime
    print 'Total time:', endTime

@@ -413,19 +413,23 @@
 C'%5D%0A    
-pre
+navAfly
  = ip.mk
@@ -429,16 +429,17 @@
 = ip.mk_
+n
 eq(ctx, 
@@ -476,21 +476,22 @@
 te)%0A    
-post1
+wpnBoc
  = ip.mk
@@ -483,33 +483,32 @@
  wpnBoc = ip.mk_
-n
 eq(ctx, weaponDe
@@ -528,21 +528,23 @@
 oc)%0A    
-post2
+wpnSboc
  = ip.mk
@@ -536,33 +536,32 @@
 wpnSboc = ip.mk_
-n
 eq(ctx, weaponDe
@@ -582,20 +582,59 @@
 oc)%0A    
-post
+# NavUpd!=AflyUpd /%5C WpnDel=BOC%0A    target1
  = ip.mk
@@ -647,20 +647,23 @@
 tx, 
-post1, post2
+navAfly, wpnBoc
 )%0A  
@@ -672,16 +672,17 @@
 # NavUpd
+!
 =AflyUpd
@@ -695,24 +695,8 @@
 nDel
-!=BOC /%5C WpnDel!
 =SBO
@@ -707,16 +707,17 @@
   target
+2
  = ip.mk
@@ -730,17 +730,69 @@
 tx, 
-pre, post
+navAfly, wpnSboc)%0A    target = ip.mk_or(ctx, target1, target2
 )%0A  

Fix to property