Now we need to find all paths to prove the path we found is the shortest path.
In order to do that, we need a new module to find all paths.
mod ALLPF is inc CONFIG2 . vars NI NI’ : NId .
vars D D’ N N’ W : Nat . var NS’ : NStat .
vars NNPs1 NNPs2 NNPs1’ NNPs2’ : Soup{NNPair} . vars NLs NLs’ : Soup{NNIDLPair} .
var OCs : Soup{OComp2}.
Above are some definitions, after are rewrite rules.
rl [fin] : {(gstat2: fin) OCs} =>{(gstat2: fin) OCs} . — makes T total.
crl [done] : {(gstat2: nFin) OCs}=>{(gstat2: fin) OCs}if done?({OCs}) .
rl [srch0] : {(gstat2: nFin) (node[NI]: visited,0,NNPs1,NNPs2,NLs) OCs}
=>{(gstat2: nFin) (node[NI]: done,0,NNPs1,NNPs2,NLs) OCs}.
rl [srch1] : {(gstat2: nFin) (node[NI]: done,0,<NI’,W>NNPs1,NNPs2,NLs) (node[NI’]: notYet,s(N’),NNPs1’,NNPs2’,NLs’) OCs}
=>{(gstat2: nFin) (node[NI]: done,0,NNPs1,<NI’,W>NNPs2,NLs) (node[NI’]:
visited,N’,NNPs1’,NNPs2’,add(NLs,NI’,W)) OCs} .
crl [srch2] : {(gstat2: nFin) (node[NI]: done,0,<NI’,W>NNPs1,NNPs2,NLs) (node[NI’]: NS’,s(N’),NNPs1’,NNPs2’,NLs’) OCs}
=>{(gstat2: nFin) (node[NI]: done,0,NNPs1,<NI’,W >NNPs2,NLs) (node[NI’]: NS’,N’,NNPs1’,NNPs2’,NLs’ add(NLs,NI’,W)) OCs}
if NS’ =/= notYet . endm
Every node has input or output or both, we count every input of a node, and then when finish calculate one input of a node, the number of input will decrease 1, and the path will be recorded, the program will finish until each number of node is decreased to 0, which means every path from each node is found.
Now we use such rewrite rules to search all paths from n0 to n63, but I encountered a problem, the amount of calculation is too large, I have waited several hours in front of the computer, but it still cannot get the paths, the program is fine, I checked it a lot times, so I have to make it half, the new graph is like this.Fig. 4.5
Figure 4.64: Finding All Path
Now n31 is the goal, then we can use such search command:
search [1] in ALLPF : init =>*{(gstat2: fin) (node[n31]: done,0,empty,NNPs2,NLs) OCs}.
donemeans all paths to this node are found.
Then we can get such result:
Solution 1 (state 209433) states: 209434 rewrites: 17407556 in 161168ms cpu (161634ms real) (108008 rewrites/second)
OCs –>(node[n0]: done,0,empty,<n1,1 ><n8,1 >,<0,n0 >) (node[n1]: done,0, empty,<n2,2 ><n9,1 >,<1,n0 ->n1>) (node[n2]: done,0,empty,<n3,1 ><n10,2 >,<3,n0 ->n1 ->n2 >) (node[n3]: done,0,empty,<n4,1 ><n11,1 >,<4,n0 ->n1 ->n2 ->n3 >) (node[n4]: done,0,empty,<n5,1 ><n12,2 >,<5,n0 ->n1 ->n2 ->n3 ->n4
>)
(node[n5]: done,0,empty,<n6,2><n13,2>,<6, n0 ->n1 ->n2 ->n3 ->n4 ->n5>)
...
For all results, please see Chapter. 8
As we can see, if there are 32 nodes on the graph, the calculation time is 161168ms, which is less than 3 minutes, and the time of calculation is exponential growth, which means every single node we add, the calculation time will grow very fast, so all paths of 64 node will not be found in a short time, in this case I just show the situation which is 32 nodes in the graph.
For this graph, there are 32 nodes, and the number of paths from node n0 to node n31 is
The number of paths from n0 to n31 which cost is 13:
2
The number of paths from n0 to n31 which cost is 14:
26
The number of paths from n0 to n31 which cost is 15:
38
The number of paths from n0 to n31 which cost is 16:
32
The number of paths from n0 to n31 which cost is 17:
16
The number of paths from n0 to n31 which cost is 18:
6
Total number:
120
So there are totally 120 paths from node n0 to node n31, and the the number of shortest paths is 2, which means there are 2 shortest paths from
13,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n15 ->n23 ->n31 13,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n14 ->n15 ->n23 ->n31 When we use the first module to search the shortest path, it will get such result:
node[n31]: 13,empty,empty,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n15 ->n23 ->n31
We can see these paths more clearly by observing the graph:
Figure 4.65: All path found 1
Figure 4.66: All path found 2 Twoblue lines are paths found by second RL.
one redline is path found by first RL.
Fig. 4.65 shows the first path found by second RL.
Fig. 4.66 shows the second path found by second RL.
Figure 4.67: Path found by first RL
As we can see from the graph, Fig. 4.65 and Fig. 4.67 is the same path, which means the path found by the first RL is one of the shortest paths.
After we found all paths from node n0 to node n31, we can manually find the shortest paths, and then use them to do model checking.
Then we can do model-checking to check some properties, in order to do model checking, we need to define two new modules:
mod DIJKSTRA-PREDS is pr DIJKSTRA .
inc SATISFACTION . subsort Config <State . ops fin isSPath : ->Prop .
op sPaths : ->Soup{NNIDLPair} . var OCs : Soup{OComp} .
var D : Nat . var L : List{NId} . var PROP : Prop .
Above are some defenitions.
eq sPaths = ( <13,n0 >n1 >n2 >n3 >n4 >n5 >n6 >n14 >n15
->n23 ->n31><13,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n14 ->n15 ->n23
->n31 >) .
Those paths are shortest paths from which I extracted from another rewrite rule.
eq {(gstat: fin) OCs} |= fin = true .
eq {(path: (<D,L >)) OCs} |= isSPath = (<D,L >
in sPaths) .
eq {OCs} |= PROP = false [owise] .
endm
mod DIJKSTRA-CHECK is inc DIJKSTRA-PREDS . inc MODEL-CHECKER . inc LTL-SIMPLIFIER . ops halt correct : ->Formula . eq halt =<>fin .
Here <>fin means true until fin is true, if fin is always false,
this will return false, so if Dijkstra never halts, it will return false, if Dijkstra always halts, it will return true.
eq correct = [](fin -><>isSPath) .
Here what after [] must always be true, otherwise will return false, if what Dijkstra found is one of the shortest paths, this will returns true
endm
This module means there are two properties that can be model checked.
The first property is whether Dijkstra always halts.
The second property is the path found by Dijkstra is one of the shortest paths.
And we can do model checking to confirm that:
red in DIJKSTRA64-CHECK : modelCheck(init,halt) .
This command is to model check the first property, whether Dijkstra always halt.
After using this command, we can get such result:
red in DIJKSTRA64-CHECK : modelCheck(init,halt) .
Advisory: reparsing module DIJKSTRA64-CHECK due to changes in imported modules.
Advisory: reparsing module DIJKSTRA64-PREDS due to changes in imported modules.
reduce in DIJKSTRA64-CHECK : modelCheck(init, halt) .
rewrites: 14083 in 65ms cpu (68ms real) (214696 rewrites/second) result Bool: true
True means Dijkstra always halt.
red in DIJKSTRA64-CHECK : modelCheck(init,correct) .
This command is to model check the second property, is the path found by Dijkstra is one of the shortest paths.
red in DIJKSTRA64-CHECK : modelCheck(init,correct) .
rewrites: 14131 in 76ms cpu (79ms real) (184304 rewrites/second) result Bool: true
And also true, which means the path found by Dijkstra is one of the shortest paths.