Changeset 31 for vis_dev/vis-2.3

Timestamp:

Dec 8, 2011, 5:23:16 PM (13 years ago)

Author:

cecile

Message:

example for _transition

Location:

vis_dev/vis-2.3/models/transition

Files:

• relation.bdd (modified) (1 diff)
• script (modified) (1 diff)
• simple.mv (modified) (1 diff)

vis_dev/vis-2.3/models/transition/relation.bdd

@@ -1 @@
-\define TRANS (state<0> = 1 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 ))+ state<1>$NS = 0 * (  p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (  state<1>$NS = 0 * (  p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))
-\define REACH (state<0> = 1 * (state<1> = 1 * (p = 1 * (q = 1 ))+ state<1> = 0 * (  p = 0 * (q = 1 )))+ state<0> = 0 * (state<1> = 1 * (p = 1 * (  q = 0))+ state<1> = 0 * (  p = 0 * (  q = 0))))
-\define REL (state<0> = 1 + state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 + state<1> = 0 * (state<1>$NS = 1 + state<1>$NS = 0 * (p = 1 + p = 0 * (q = 1 ))))+ state<0>$NS = 0))
-\define new_rel (state<0> = 1 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 ))+ state<1>$NS = 0 * (  p$NS = 0 * (q$NS = 1 ))))+ state<0>$NS = 0 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (state<1>$NS = 1 * (p$NS = 1 * (q$NS = 1 )))+ state<1> = 0 * (  state<1>$NS = 0 * (p = 1 * (  p$NS = 0 * (q$NS = 1 ))+ p = 0 * (  p$NS = 0 * (q = 1 * (q$NS = 1 ))))))+ state<0>$NS = 0 * (state<1>$NS = 1 * (p$NS = 1 * (  q$NS = 0)))))
+\define TRANS_6 (state<0> = 1 * (  state<1> = 0 * (i = 1 ))+ state<0> = 0 * (state<0>$NS = 1 * (  state<1> = 0 * (state<1>$NS = 1 * (i = 1 )))+ state<0>$NS = 0 * (  state<1> = 0 * (i = 1 ))))
+\define TRANS_6 (state<0> = 1 * (state<1> = 1 + state<1> = 0 * (  i = 0))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 + state<1> = 0 * (state<1>$NS = 1 * (  i = 0)))+ state<0>$NS = 0 * (state<1> = 1 + state<1> = 0 * (  i = 0))))
+\define TRANS_8 (state<0> = 1 * (state<1> = 1 * (i = 1 ))+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (state<1>$NS = 1 * (  i = 0)))+ state<0>$NS = 0 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (  i = 0))))
+\define TRANS_8 (state<0> = 1 * (state<1> = 1 * (  i = 0)+ state<1> = 0)+ state<0> = 0 * (state<0>$NS = 1 * (state<1> = 1 * (  i = 0)+ state<1> = 0 * (state<1>$NS = 1 * (i = 1 )))+ state<0>$NS = 0 * (state<1> = 1 * (  i = 0)+ state<1> = 0 * (i = 1 ))))
+\define TRANS_1 (state<0> = 1 * (state<1> = 1 * (i = 1 ))+ state<0> = 0 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (  i = 0)))
+\define TRANS_1 (state<0> = 1 * (state<1> = 1 * (  i = 0)+ state<1> = 0)+ state<0> = 0 * (state<1> = 1 * (  i = 0)+ state<1> = 0 * (state<1>$NS = 1 * (i = 1 ))))
+\define TRANS_3 (state<0> = 1 * (  state<1> = 0 * (i = 1 ))+ state<0> = 0 * (  state<0>$NS = 0 * (  state<1> = 0 * (i = 1 ))))
+\define TRANS_3 (state<1> = 1 + state<1> = 0 * (  i = 0))

vis_dev/vis-2.3/models/transition/script

@@ -2 +2 @@
 init
 compute_reach -v 1 
-transition
+_transition

vis_dev/vis-2.3/models/transition/simple.mv

@@ -1 +1 @@
 # vl2mv simple.v 
 # version: 2.1
-# date:    14:23:27 12/01/2011 (CET)
+# date:    16:16:51 12/06/2011 (CET)
 .model concret 
 # I/O ports