# [PVS-Help] Need help with the Choose function

 Hello all- I need help with the choose function. I want to choose the edge from X in my graph and there is only one from (X,Y) however the choose function returns (Y,Z).   The below theorem is is trying to prove that an edge can be taken (ie taken=true).   However all my code has been simplified down to just just trying to get an outgoing edge from the X vert in the graph. If my choose function picks the only edge in the graph from X then the PC counter would go to LTRUE which gets taken=true.  However right now the choose function always pick (Y,Z).   I do not know where I'm going wrong, unless i'm just not using the right commands to prove it.   Any help at all would be greatly appreciated.   Kelly         %Initialize graph InitGraph: digraph[Entity] = (#vert:= add(X, add(Y, singleton[Entity](Z))), edges:= add((X,Y), add((Y,Z),emptyset[edgetype]))#)   I have a node type which is declared:   node : TYPE = [# dest: Entity, % destination source: Entity, % source edge starts from e1: edgetype, % an outgoing edge ie: finite_set[edgetype], % all incoming edges oe: finite_set[edgetype], % all outgoing edges oec: nat, %outgoing edge card iec:nat % incomiing edge card #]   And a node database type declared as a function. as each entity in the graph has node data attached to it. n_db: TYPE = function[Entity -> node]     PVS file below. (the files is also attached as ptakerule.pvs, tdd.pvs is the definition theory it imports.) ---------------------------------------------------------------------------------------------------------- pt %[Entity: TYPE+]: THEORY %SUBJECT ONLY %Is used strictly for the 3 node query, which is how the rule is defined. BEGIN Importing tDefinitions%[Entity]   %Initialize graph InitGraph: digraph[Entity] = (#vert:= add(X, add(Y, singleton[Entity](Z))), edges:= add((X,Y), add((Y,Z),emptyset[edgetype]))#)   %initializes the edge rights ADD(db: r_db): r_db = db with [(X,Y):= add(take, emptyset[Rights])] with [(Y,Z):= add(read,emptyset[Rights])]   %---------------------------------------------------------------------------------------- set_edge(x:Entity,a:edgetype, c:L_Graph,oes: finite_set[edgetype] ): L_Graph = c with [`Node(x)`e1:=a,`Node(x)`oe:=oes ]   get_edge(c: L_Graph, x: Entity): L_Graph = %see if the current edge has take for a right if it does update the dest and source if empty?(c`Node(x)`oe) then c else let a = choose(c`Node(x)`oe) in set_edge(x,a, c, rest(c`Node(x)`oe)) endif   XYedge?(c:L_Graph, x:Entity):bool = member((X,Y),c`Node(x)`oe) % this should return true for X   YZedge?(c:L_Graph, x:Entity):bool = member((Y,Z),c`Node(x)`oe) % this should return false for X   e1?(c:L_Graph, x:Entity):bool= member(c`Node(x)`e1,c`Node(x)`oe) %---------------------------------------------------------------------------------------- %loop actions %sets: one   L0(c: L_Graph, x:Entity, y:Entity): L_Graph = c with [%g0:= InitGraph, g1:=InitGraph, db:= ADD(c`db), one:=x ]   %sets the node var oe to the outgoing edges and the node variable ie to the incoming edges get_out_in_edge(x:Entity,oes: finite_set[edgetype], ies: finite_set[edgetype], c:L_Graph): L_Graph = c with [`Node(x)`source:=x,`Node(x)`oe:=oes, `Node(x)`ie:=ies ]   TAKE(c: L_Graph, x: Entity, n: n_db):L_Graph = get_edge(c,x)   LTRUE(c:L_Graph): L_Graph = c with [taken:= true] LFALSE(c:L_Graph): L_Graph = c with [taken:= false] %---------------------------------------------------------------------------------------- %Loop sw(c: L_Graph, r: Rights, x: Entity, y: Entity): L_Graph = Cases c`PC of %initializes graph and r_db % checks if first node is in graph else quit L0:L0(c,x,y) with [PC:=L1],   %checks if there are at least 3 verts in graph else quit L1: c with [PC:= if (card[Entity](vert(c`g1))>=3) then L2 else LFALSE endif],   L2: get_out_in_edge(x,outgoing_edges(x, c`g1), incoming_edges(x, c`g1), c) with [PC:= L3], %TAKE   L3: c with [PC:=if XYedge?(c, x) then L4 else LFALSE endif], %TAKE   L4:c with [PC:=if YZedge?(c, x) then LFALSE else TAKE endif],   TAKE: TAKE(c, c`one, c`Node) with [PC:=L5], %TAKE1   L5: c with [PC:=if e1?(c, x) then LTRUE else LFALSE endif],   LTRUE: LTRUE(c) with [PC:= LEND],   LFALSE:LFALSE(c) with [PC:= LEND],   LEND: c Endcases   takerule(num: nat, r: Rights, x: Entity, y: Entity, initial: L_Graph ): Recursive L_Graph = if num=0 then initial with [PC:=L0] else sw(takerule(num-1,r,x,y,initial),r,x,y) endif measure num   Take_Rule_Taken: theorem forall (initial: L_Graph): forall(num: nat | takerule(num, read, X, Z, initial)`PC=LEND): takerule(num, read, X, Z, initial)`taken=true   %(skosimp)(induct "num")(grind)(grind)(induct "j")(grind)(grind)(expand "takerule")(expand "takerule")(grind)(expand "takerule")(expand "takerule")(grind) % %(rewrite "card_add")(rewrite "card_add")(rewrite "card_singleton")(grind)   END ptMake distant family not so distant with Windows Vista® + Windows Live™. Start now!
```tDefinitions %[Entity: TYPE+]
: THEORY

BEGIN
Entity: Type = {X,Y,Z}
Importing digraphs@digraphs[Entity]
Importing digraphs@digraph_ops[Entity]
Importing digraphs@digraph_deg[Entity]

%declares TYPE of right works
Rights: TYPE = {read, write, take, grant}

PCT: TYPE = {L0,L00,L3,L31,L20, L01, L001,L0001,L00001, L02,L1,L2,L4,L41,L5,L8,L10,L81,LTRUE,LFALSE,TAKE,TAKE1 ,LEND}

% don't put + on the Types following

r_db: TYPE =function[edgetype[Entity]->set[Rights]]
nil: Entity

node : TYPE = [#
dest: Entity, % destination
source: Entity, % source edge starts from
e1: edgetype, % an outgoing edge
ie: finite_set[edgetype], % all incoming edges
oe: finite_set[edgetype], % all outgoing edges
oec: nat,
iec:nat

#]

%nodes: TYPE = set[node]
n_db: TYPE = function[Entity -> node]
L_Graph: TYPE = 	[#
%	g0: digraph[Entity],
g1: digraph[Entity],
db: r_db,
PC: PCT,
Node: n_db,
taken: bool,
one:   Entity,
two:  Entity,
three: Entity
#]

null: edgetype = (nil,nil)
%X,Y,Z: Entity

END tDefinitions
```

ptakerule.pvs