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

*To*: pvs-help@csl.sri.com*Subject*: Help with choose and epsilon*From*: Darryl Scott Dieckman <ddieckma@ececs.uc.edu>*Date*: Wed, 6 May 1998 16:55:16 -0400 (EDT)

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

- Prev by Date:
**Re: What have I missed ? (a proof failed)** - Next by Date:
**Help with choose (pvs dump file)** - Prev by thread:
**Help with choose (pvs dump file)** - Next by thread:
**Re: Help with choose and epsilon** - Index(es):