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

Re: Help with choose and epsilon



choose is carefully defined so the property you want is encoded in
its type.  There's some explanation of this in the paper at
  http://www.csl.sri.com/tse98.html
You have to explicitly bring in the appropriate type constraints with
the typepred command.

Thus, one branch of your proof can be dealt with as shown below
(I haven't tried the other branch).

John





chosen_node_outputs :  

  |-------
{1}    (FORALL (net: Network, node: Node, pkt: Packet):
         member(node, net) AND dest(pkt) = addr(node)
             IMPLIES nonempty?(outQ(chooseNode(nextState(pkt, net)))))

Rule? (SKOSIMP)
Skolemizing and flattening,
this simplifies to: 
chosen_node_outputs :  

{-1}    member(node!1, net!1)
{-2}    dest(pkt!1) = addr(node!1)
  |-------
{1}    nonempty?(outQ(chooseNode(nextState(pkt!1, net!1))))

Rule? (EXPAND "chooseNode")
Expanding the definition of chooseNode,
this simplifies to: 
chosen_node_outputs :  

[-1]    member(node!1, net!1)
[-2]    dest(pkt!1) = addr(node!1)
  |-------
{1}    IF
          nonempty?(filter(nextState(pkt!1, net!1),
                           (LAMBDA (n: Node): nonempty?(outQ(n)))))
        THEN
        nonempty?(outQ(choose(filter(nextState(pkt!1, net!1),
                                     (LAMBDA (n: Node):
                                        nonempty?(outQ(n)))))))
      ELSE nonempty?(outQ(choose(nextState(pkt!1, net!1))))
      ENDIF

Rule? (GROUND)
Applying propositional simplification and decision procedures,
this yields  2 subgoals: 
chosen_node_outputs.1 :  

{-1}    nonempty?(filter(nextState(pkt!1, net!1),
                       (LAMBDA (n: Node): nonempty?(outQ(n)))))
[-2]    member(node!1, net!1)
[-3]    dest(pkt!1) = addr(node!1)
  |-------
{1}    nonempty?(outQ(choose(filter(nextState(pkt!1, net!1),
                                   (LAMBDA (n: Node):
                                      nonempty?(outQ(n)))))))

Rule? (TYPEPRED "choose(filter(nextState(pkt!1, net!1),
                                   (LAMBDA (n: Node):
                                      nonempty?(outQ(n)))))")

Adding type constraints for  choose(filter(nextState(pkt!1, net!1),
                                   (LAMBDA (n: Node):
                                      nonempty?(outQ(n))))),
this simplifies to: 
chosen_node_outputs.1 :  

{-1}    filter(nextState(pkt!1, net!1),
             (LAMBDA (n: Node):
                nonempty?(outQ(n))))(choose(filter(nextState(pkt!1, net!1),
                                                   (LAMBDA (n: Node):
                                                      nonempty?(outQ(n))))))
[-2]    nonempty?(filter(nextState(pkt!1, net!1),
                       (LAMBDA (n: Node): nonempty?(outQ(n)))))
[-3]    member(node!1, net!1)
[-4]    dest(pkt!1) = addr(node!1)
  |-------
[1]    nonempty?(outQ(choose(filter(nextState(pkt!1, net!1),
                                   (LAMBDA (n: Node):
                                      nonempty?(outQ(n)))))))

Rule? (EXPAND "filter")
Expanding the definition of filter,
this simplifies to: 
chosen_node_outputs.1 :  

{-1}    nextState(pkt!1,
                net!1)(choose({x: Node |
                              nextState(pkt!1, net!1)(x) & nonempty?(outQ(x))}))
          &
        nonempty?(outQ(choose({x: Node |
                              nextState(pkt!1,
                                        net!1)(x)
                                  &
                                nonempty?(outQ(x))})))
{-2}    nonempty?({x: Node | nextState(pkt!1, net!1)(x) & nonempty?(outQ(x))})
[-3]    member(node!1, net!1)
[-4]    dest(pkt!1) = addr(node!1)
  |-------
{1}    nonempty?(outQ(choose({x: Node |
                            nextState(pkt!1,
                                      net!1)(x)
                                &
                              nonempty?(outQ(x))})))

Rule? (GROUND)
Applying propositional simplification and decision procedures,

This completes the proof of chosen_node_outputs.1.

chosen_node_outputs.2 :  

[-1]    member(node!1, net!1)
[-2]    dest(pkt!1) = addr(node!1)
  |-------
{1}    nonempty?(filter(nextState(pkt!1, net!1),
                       (LAMBDA (n: Node): nonempty?(outQ(n)))))
{2}    nonempty?(outQ(choose(nextState(pkt!1, net!1))))

Rule? 
-------