Changeset 31 for vis_dev


Ignore:
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:
3 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/models/transition/relation.bdd

    r28 r31  
    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)))))
    2 \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))))
    3 \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))
    4 \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)))))
     1\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 ))))
     2\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))))
     3\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))))
     4\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 ))))
     5\define TRANS_1 (state<0> = 1 * (state<1> = 1 * (i = 1 ))+ state<0> = 0 * (state<1> = 1 * (i = 1 )+ state<1> = 0 * (  i = 0)))
     6\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 ))))
     7\define TRANS_3 (state<0> = 1 * (  state<1> = 0 * (i = 1 ))+ state<0> = 0 * (  state<0>$NS = 0 * (  state<1> = 0 * (i = 1 ))))
     8\define TRANS_3 (state<1> = 1 + state<1> = 0 * (  i = 0))
  • vis_dev/vis-2.3/models/transition/script

    r28 r31  
    22init
    33compute_reach -v 1
    4 transition
     4_transition
  • vis_dev/vis-2.3/models/transition/simple.mv

    r28 r31  
    11# vl2mv simple.v
    22# version: 2.1
    3 # date:    14:23:27 12/01/2011 (CET)
     3# date:    16:16:51 12/06/2011 (CET)
    44.model concret
    55# I/O ports
Note: See TracChangeset for help on using the changeset viewer.