[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Help with choose and epsilon

I have been trying to use choose to select an arbitrary element 
from a set, and have been unsuccessful trying to prove anything.

I have included the .dmp file for reference.  My specification
is modeling the components in a computer network.  The network
is a set of nodes, where each node has a queue of packets to 
transmit.  I would like to be able to specify a nextState function
for the network that selects an arbitrary packet from any node 
that has pending packets and then process that packet.  

Eventually I would like to show that some invariants hold over the
network regardless of which packet is selected to be processed.

Should I be trying to use choose() to accomplish this?

I tried to prove 'chosen_node_outputs' but got stuck when I
got to the epsilon term.  

Is there a better way to specify that an invariant will hold 
no matter which packet I select?  I've been trying to figure this out 
for at least a week, and haven't had much luck.  Any suggestions,
pointers, criticisms, would be Greatly appreciated.

Thank you
Darryl Dieckman