template for analysis

Author: yarden

analysis/mojo_utils.py

@@ -0,0 +1,22 @@
+import os
+import sys
+import time
+
+OUTDIR = os.path.abspath("../outputs/")
+SNAPDIR = os.path.abspath("../snapshots/")
+
+def get_model_info(model_name):
+    info = {"snap_fname": None,
+            "out_fname": None}
+    snap_fname = os.path.join(SNAPDIR, "%s.json" %(model_name))
+    out_fname = os.path.join(OUTDIR, "%s.out" %(model_name))
+    if os.path.isfile(snap_fname):
+        info["snap_fname"] = snap_fname
+    else:
+        raise Exception("Could not find snapshot %s for %s" %(model_name,
+                                                              snap_fname))
+    if os.path.isfile(out_fname):
+        info["out_fname"] = out_fname
+    return info
+        
+    

analysis/simple_chain.py

@@ -0,0 +1,6 @@
+## Analyze simple chain model
+import mojo_utils
+
+info = mojo_utils.get_model_info("simple_chain")
+print("Model information for simple chain: ")
+print(info)

models/simple_chain.ka

@@ -17,4 +17,4 @@
 %obs: 'atleast_two_chain' |C(x,y[1]),C(x[1],y)|
 %obs: 'exactly_two_chain' |C(x[.],y[1]),C(x[1],y[.])|
 
-%mod: alarm 1000.0 do $STOP "../snapshots/simple_chain";
+%mod: alarm 100000.0 do $STOP "./snapshots/simple_chain.json";

run_models.py

@@ -12,6 +12,8 @@
 OUTDIR = "./outputs/"
 SNAPDIR = "./snapshots/"
 
+SEED = 10
+
 def check_KaSim():
     """
     Check if KaSim is available on path.
@@ -31,18 +33,19 @@ def run_KaSim(model_fname):
     model_name = model_basename.split(".ka")[0]
     dir_name = os.path.dirname(model_fname)
     out_fname = os.path.join(OUTDIR, "%s.out" %(model_name))
-    snapshot_fname = os.path.join(SNAPDIR, model_basename)
+    snapshot_fname = os.path.join(SNAPDIR, "%s.json" %(model_name))
     # remove older output/snapshot files
     older_files = [out_fname, snapshot_fname]
     for old_fname in older_files:
         if os.path.isfile(old_fname):
             print("Removing previous file: %s" %(old_fname))
             os.unlink(old_fname)
     print("Running %s" %(model_basename))
-    # run KaSim (and don't generate log files)
+    # run KaSim: don't generate log files and use seed
     cmd = \
-       '''KaSim --no-log -o {out_fname} {model_fname}'''.format(out_fname=out_fname,
-                                                                model_fname=model_fname)
+       '''KaSim --no-log -seed {seed} -o {out_fname} {model_fname}'''.format(out_fname=out_fname,
+                                                                             model_fname=model_fname,
+                                                                             seed=SEED)
     ret_val = os.system(cmd)
     if ret_val != 0:
         raise Exception("Failed to execute %s" %(cmd))

snapshots/simple_chain.json

@@ -0,0 +1 @@
+{"snapshot_file":"./snapshots/simple_chain.json","snapshot_event":161977,"snapshot_time":100000.0,"snapshot_agents":[[1,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[11,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[4,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[5,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[3,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[6,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[4,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[7,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[5,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[8,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[6,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[9,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[7,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[10,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[8,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[9,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[0,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[12,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[11,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[13,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[12,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[14,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[13,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[15,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[14,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[16,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[15,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[17,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[16,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]],[1,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[4,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[0,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[5,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[4,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[6,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[5,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[7,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[6,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[8,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[7,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[9,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[8,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[10,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[9,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[11,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[10,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]],[1,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[6,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[4,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[5,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[3,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[4,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[0,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[7,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[6,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[8,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[7,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[9,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[8,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]],[1,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[5,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[4,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[3,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[0,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[6,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[5,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[7,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[6,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[8,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[7,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]],[1,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[4,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[5,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[3,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[6,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[4,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[5,0]],"port_states":[]}]}]}]],[2,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[5,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[4,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[3,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[0,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]],[2,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[2,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[3,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]}]],[3,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[1,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[0,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[2,0]],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]],[4,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[[1,1]],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]},{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[[0,0]],"port_states":[]}]}]}]],[7,[{"node_type":"C","node_sites":[{"site_name":"x","site_type":["port",{"port_links":[],"port_states":[]}]},{"site_name":"y","site_type":["port",{"port_links":[],"port_states":[]}]}]}]]],"snapshot_tokens":[]}