[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.