Hi Vanessa,
+-----+
| v
1->2->3->4->5->6->7
^ | | |
+-----+--+--------+
> sir
> i have attached one state diagram.z(output) is true at
> states 3 and 4.
> (1)VIS evaluate AX(z) in following steps
>
> AXz = -EX-z = -EX-[3,4] = -EX[1,2,5,6,7]
> = -[3,7,1,4,5,6] = [2]
I agree, if we don't add the reset edges.
> (2)VIS evaluate AF(state7) in following steps
>
> AF[7] = -EG-[7] = -EG[1,2,3,4,5,6] = -[(1,2,3),(1,2,4)]
> -[1,2,3,4] = [3,4,5]
Yes, although -[1,2,3,4] = [5,6,7]. Again, this only holds if we do not
take the reset edges into account.
> Fot the state diagram this is also true that whenever
> reset occurs next state will be state1.These transitions
> are not shown in the diagram.
> I want to ask,what is the similar proof for
> AG( reset -> AX state1);
> This statement is equivalent to
> AG(-reset + AXstate1),but which states i should take corresponding to > reset which is an external input.
Good question. This is one of the reasons that you cannot use primary
inputs in vis. You would be asking questions about edges instead of
states, and I don't know how to interpret those, either.
If you latch reset, you effectively double the state space. A state
with number n gets split into a state n_0, in which reset is false, and
a state n_1, in which reset is true. From n_1 you would only have an
edge to 1_0 and 1_1, whereas from n_0 you would have edges according to
your state diagram. For example, 5_0 would have an edge to 6_0 and 6_1.
If you do that, the proof becomes easy. AX[1] =
[3_0,7_0,1_1,2_1,3_1,4_,5_1,6_1,7_1]. -reset=
[1_0,2_0,3_0,4_0,5_0,6_0,7_0], so -reset + AX[1] =
[1_0,2_0,3_0,4_0,5_0,6_0,7_0,1_1,2_1,3_1,4_,5_1,6_1,7_1], and AG(-reset
+ AX[1]) = [1_0,2_0,3_0,4_0,5_0,6_0,7_0,1_1,2_1,3_1,4_,5_1,6_1,7_1],
which makes it true, regardless of the initial state.
I hope this helps. Let me know if it is confusing.
Roderick.
This archive was generated by hypermail 2b30 : Fri May 25 2001 - 09:44:02 MDT