JAIST Repository: Investigation and Specification of Path Finding Algorithms [課題研究報告書]

(1)

JAIST Repository

https://dspace.jaist.ac.jp/

Title Investigation and Specification of Path Finding Algorithms [課題研究報告書]

Author(s) 楊, 子

Citation

Issue Date 2019-03

Type Research Paper

Text version author

URL http://hdl.handle.net/10119/15923

Rights

Description Supervisor:Kazuhiro Ogata, 先端科学技術研究科, 修

(2)

Master’s Research Project Report

Investigation and Specification of Path Finding Algorithms

1710282 Yang Zi

Supervisor Kazuhiro Ogata Main Examiner Kazuhiro Ogata

Examiners Kunihiko Hiraishi Toshiaki Aoki Masato Suzuki

Graduate School of Advanced Science and Technology Japan Advanced Institute of Science and Technology

(Information Science)

(3)

Acknowledgements

I would like to express my gratitude to all those who helped me during the writing of this Master project report. I gratefully acknowledge the help of my supervisor, Prof. Ogata Kazuhiro, who has offered me valuable suggestions in studies, In the preparation of the report he has spent much time providing me with inspiring advice. Without his patient instruction, the completion of this thesis would not have been possible.

I also have to thank my parents who have always been helping me out of difficulties and supporting with a word of complaint.

I should finally like to thank all of my friends who helped me a lot in JAIST.

(4)

One of the most important technologies for automatic driving cars is the automatic pathfinding algorithm, which decides the path the car is going, we can use some diagrams to represent the real world situation, which has some nodes to represent some cross of the road, using cost to represent the distance of the road, and then we have a start node and a goal, using pathfinding algorithm, we can know the shortest path from the start node to the goal. There are many different pathfinding algorithms, one of which is the Dijkstra shortest path algorithm.

To verify the reliability of these algorithms, model checking is required. To check if they can enjoy some desired properties. model checking is giving a model of a system, automatically check whether this model enjoys some properties. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of dead-locks and similar critical states that can cause the system to crash. Model checking is a technique for automatically verifying correctness properties of finite-state systems.

This paper show a case of pathfinding algorithms Dijkstra, after formal-izing Dijkstra to state machine and feed into Maude, we can see the state transition, and then we can do model checking using some desired properties.

(7)

List of Figures

2.1 Kripke structure . . . 3 2.2 LTL temporal operators . . . 4 2.3 Next operator . . . 5 2.4 Finally operator . . . 5 2.5 Globally operator . . . 5 2.6 Until operator . . . 5 2.7 Dijkstra step0 . . . 6 2.8 Dijkstra step1 . . . 7 2.9 Dijkstra step2 . . . 7 2.10 Dijkstra step3 . . . 7 2.11 Dijkstra step4 . . . 8 2.12 Dijkstra step5 . . . 8 2.13 Dijkstra step6 . . . 9 2.14 Maude display . . . 10

3.1 Real World Model . . . 13

3.2 Dijkstra . . . 14 4.1 Nodes Visited 1 . . . 16 4.2 Nodes Visited 2 . . . 16 4.3 Nodes Visited 3 . . . 17 4.4 Nodes Visited 4 . . . 17 4.5 Nodes Visited 5 . . . 17 4.6 Nodes Visited 6 . . . 17 4.7 Nodes Visited 7 . . . 17 4.8 Nodes Visited 8 . . . 17 4.9 Nodes Visited 9 . . . 18 4.10 Nodes Visited 10 . . . 18 4.11 Nodes Visited 11 . . . 18 4.12 Nodes Visited 12 . . . 18 4.13 Nodes Visited 13 . . . 18 4.14 Nodes Visited 14 . . . 18

(8)

4.15 Nodes Visited 15 . . . 19 4.16 Nodes Visited 16 . . . 19 4.17 Nodes Visited 17 . . . 19 4.18 Nodes Visited 18 . . . 19 4.19 Nodes Visited 19 . . . 19 4.20 Nodes Visited 20 . . . 19 4.21 Nodes Visited 21 . . . 20 4.22 Nodes Visited 22 . . . 20 4.23 Nodes Visited 23 . . . 20 4.24 Nodes Visited 24 . . . 20 4.25 Nodes Visited 25 . . . 20 4.26 Nodes Visited 26 . . . 20 4.27 Nodes Visited 27 . . . 21 4.28 Nodes Visited 28 . . . 21 4.29 Nodes Visited 29 . . . 21 4.30 Nodes Visited 30 . . . 21 4.31 Nodes Visited 31 . . . 21 4.32 Nodes Visited 32 . . . 21 4.33 Nodes Visited 33 . . . 22 4.34 Nodes Visited 34 . . . 22 4.35 Nodes Visited 35 . . . 22 4.36 Nodes Visited 36 . . . 22 4.37 Nodes Visited 37 . . . 22 4.38 Nodes Visited 38 . . . 22 4.39 Nodes Visited 39 . . . 23 4.40 Nodes Visited 40 . . . 23 4.41 Nodes Visited 41 . . . 23 4.42 Nodes Visited 42 . . . 23 4.43 Nodes Visited 43 . . . 23 4.44 Nodes Visited 44 . . . 23 4.45 Nodes Visited 45 . . . 24 4.46 Nodes Visited 46 . . . 24 4.47 Nodes Visited 13 . . . 24 4.48 Nodes Visited 48 . . . 24 4.49 Nodes Visited 49 . . . 24 4.50 Nodes Visited 50 . . . 24 4.51 Nodes Visited 51 . . . 25 4.52 Nodes Visited 52 . . . 25 4.53 Nodes Visited 53 . . . 25 4.54 Nodes Visited 54 . . . 25

(9)

4.56 Nodes Visited 56 . . . 25 4.57 Nodes Visited 57 . . . 26 4.58 Nodes Visited 58 . . . 26 4.59 Nodes Visited 59 . . . 26 4.60 Nodes Visited 60 . . . 26 4.61 Nodes Visited 61 . . . 26 4.62 Nodes Visited 62 . . . 26 4.63 Nodes Visited 63 . . . 27

4.64 Finding All Path . . . 34

4.65 All path found 1 . . . 36

4.66 All path found 2 . . . 36

4.67 Path found by first RL . . . 37

5.1 The 2nd graph . . . 40

5.2 The 3rd graph . . . 42

5.3 The 4th graph . . . 43

5.4 The 4th graph . . . 44

6.1 Work done in this report . . . 46

(10)

Chapter 1 Introduction

1.1 Overview

We have many pathfinding algorithms used in variety of autonomous robot such as rescue robot, which is developed to save people during heavy disaster such as fire, earthquake, nuclear radiation, as we all know, the scene of those environments are complex and very dangerous, and its difficult to rescue with human beings, rescue robot is small and smart so that they can replace human to take part in some rescue mission that human can’t. And such a rescue robot needs a pathfinding algorithm to find a perfect path. And such a path must be trustworthy and stable, the goal of this thesis is to find a pathfinding algorithm and do model checking to check whether this algorithm enjoys some properties.

The navigation modular is designed for an autonomous robot to search disaster environment. Object points are generated, then robot obtains an optimal path from starting point to target point by global path planning algorithm, such as Dijkstra.

Such a pathfinding algorithm is very important for the automatic robot, and it is also important to find out whether this algorithm is trustworthy.

1.2 Aim and Contribution

The paper reports on a case of Dijkstra, a pathfinding algorithm, after for-malize it to a state machine, we can the states transition and it is specified as a state machine in Maude so that the Maude search command and the Maude LTL model checker can be used to check some properties of Dijkstra.

(11)

1.3 Significance

We know that in the field of artificial intelligence, the automatic pathfind-ing algorithm has been widely concerned as an effective way to improve the robot’s efficiency. At present, in the field of artificial automation, auto-matic pathfinding algorithm has been studied by many scholars, and new automatic pathfinding algorithms emerge in endlessly. However, after the author’s research and investigation found that researchers in this field are currently limited to the calculation and research of automatic algorithms, but Whether the automatic algorithm itself is feasible and reliable is not studied by scholars.

However, it is worth noting that only researching the automatic pathfind-ing algorithm and related robots cannot completely solve the damage prob-lem of mobile robots. We should strengthen the detection of the reliability of the automatic pathfinding algorithm. Because only the high reliability of the automatic pathfinding algorithm can effectively reduce the damage of the robot, making the robot move more stable and efficient.

Through this report’s research on automatic pathfinding algorithm, The author wants to achieve the detection of the effectiveness of various automatic pathfinding algorithms, in order to find and develop a reliable automatic pathfinding algorithm, the best detection means, the manual automation is more stable, more Good service to humans.

1.4 Report Outline

The rest of this report is organized as follows: Chapter. 2 Preliminries

Introduces some preliminaries, such as state machine, invariant, Kripke structure and LTL, Dijkstra and Maude.

Chapter. 3 Proposed Model

This chapter shows a real-world model, and formalizes such model as a graph.

Chapter. 4 Model Checking of Dijkstra

This chapter formalizes Dijkstra to state machine, and do model checking. Chapter. 5 More Tests

This chapter uses more test to do model checking. Chapter. 6 Discussion

This chapter is to discuss the result. Chapter. 7 Conclusion

(12)

Chapter 2 Preliminaries

2.1 Kripke Structure and Linear Temporal

Logic

A Kripke structure K is hS, I, T, P, Li, where S is a set of states, I ⊆ S is the set of initial states, T ⊆ S × S is a total binary relation over S, P is a set of atomic propositions and L is a labeling function whose type is S → 2P_.

Each element (s, s0) ∈ T is called a state transition from s to s0 and T may be called the state transitions (with respect to K). For a state s ∈ S, L(s) is the set of atomic propositions that hold in s. A path π is an infinite sequence s0, . . . , si, si+1, . . . of states such that si ∈ S and (si, si+1) ∈ T for each i. Let

πi be si, si+1, . . . and π(i) be si. Let P be the set of all paths. π is called a

computation if π(0) ∈ I. Let C be the set of all computations.

Figure 2.1: Kripke structure

The syntax of a formula ϕ in LTL for K is ϕ ::= > | p | ¬ϕ | ϕ ∧ ϕ | ϕ | ϕ U ϕ, where p ∈ P . Let F be the set of all formulas in LTL for K. An arbitrary path π ∈ P of K and an arbitrary LTL formula ϕ ∈ F of K, K, π |= ϕ is inductively defined as K, π |= >, K, π |= p iff p ∈ L(π(0)),

(13)

K, π |= ¬ϕ1 iff K, π 6|= ϕ1, K, π |= ϕ1 ∧ ϕ2 iff K, π |= ϕ1 and K, π |= ϕ2,

K, π |= ϕ1 iff K, π1 |= ϕ1, and K, π |= ϕ1 U ϕ2 iff there exists a natural

number i such that K, πi _{|= ϕ}

2 and for all natural numbers j < i, K, πj |= ϕ1,

where ϕ1 and ϕ2 are LTL formulas. Then, K |= ϕ iff K, π |= ϕ for each

computation π ∈ C of K. The temporal connectives and U are called the next connective and the until connective, respectively. The other logical and temporal connectives are defined as usual as follows: ⊥ , ¬>, ϕ1 ∨ ϕ2 ,

¬(¬ϕ1∧ ¬ϕ2), ϕ1 ⇒ ϕ2 , ¬ϕ1∨ ϕ2, ♦ ϕ , > U ϕ, and ϕ , ¬(♦ ¬ϕ). The

temporal connectives ♦ and are called the eventually connective and the always connective, respectively.

State machines and their properties can be used to formalize various systems and their requirements. Systems verification can then be conducted by theorem proving that state machines enjoy properties.

A state predicate p is invariant w.r.t.M iff (∀ s ∈ R) p (s).

A state predicate p can be interpreted as a set P of states s.t.(∀ s ∈ P) p(s) and (∀ s /∈ P) ¬p(s) .

Figure 2.2: LTL temporal operators In unary operators oφ, ♦ φ, φ:

oφ is next opeartor that φ has to hold at next state. Like Fig. 2.3

♦ φ is finally operator that φ eventually has to hold (somewhere on the subsequent path).

(14)

Figure 2.3: Next operator Like Fig. 2.4

Figure 2.4: Finally operator

φ is globally operator that φ has to hold on the entire subsequent path. Like Fig. 2.5

Figure 2.5: Globally operator In binary operators such as φ U ψ:

φ U ψ is until operator that φ has to hold at least until ψ becomes true, which must hold at the current or a future position.

Like Fig. 2.6

Figure 2.6: Until operator Here:

♦ ϕ , > U ϕ ϕ , ¬(♦ ¬ϕ)

Are most important formulas used to check two properties, when checking some property such as ”whether Dijkstra always halts”, we can use the first formula. the until operator U is if ϕ never true, then ♦ ϕ returns false, if there is a case such that ϕ always true at some point, then ♦ ϕ returns true. The second formula can be used to check some property such as ”whether path found by Dijkstra is one of the shortest paths”, ϕ means ϕ has to be true until and including the point where False first becomes true; if False

(15)

This project report is using such two formulas to check the two properties mentioned above.

2.2 Dijkstra: A Path Finding Algorithm

Dijkstra’s algorithm is an algorithm for finding the shortest paths between nodes in a graph.

Here is a demo for Dijkstra see Fig. 2.7:

There are 6 nodes in this graph, each node has some neighbors, and the cost from one node to another is given, if n0 is the initial node and n5 is the final node, we can use some pathfinding algorithms like Dijkstra to find a shortest path from n0 to n5.

We suppose there are two sets S and U, set S contains the nodes which are visited, set U contains the nodes which are not visited. If a node’s shortest path is found from the initial node, we can add it to set U, when there is no element in set S, the algorithm is finished.

initially, we have S = {n0,n1,n2,n3,n4,n5}, U = {}.

Figure 2.7: Dijkstra step0

Fig. 2.8 First, since the n0 is the initial node, the which shortest path is 0, so we add this node to set U, and mark it as visited. In this graph, green represents visited. and we can know the cost from node n0 to node n1 and node n2, for the rest nodes, we mark the cost as infinity. and we choose a smallest cost which is n1, we mark n1 as visited, and the shortest path from n0 to n1 is n0=⇒n1, cost is 1. Now set S = {n1,n2,n3,n4,n5}, U = {n0}.

Fig. 2.9 Then we start to visit node n1, and we update the cost from n1 to n2 and n1 to n3, if the updated cost is smaller than current cost, we use the updated cost, if the updated cost is bigger or equal than the current cost, we don’t update it, so the cost from n0 to n1 to n2 is 2, smaller than the current cost from n0 to n2, so the current path from n0 to n2 is n0=⇒n1=⇒n2, the

(16)

(2).png

than inifity, so we update the path from n0 to n3 is n0=⇒n1=⇒n3. Then we choose a smallest cost in current nodes, which is n2, then we mark n2 as visited. Now set S = {n2,n3,n4,n5}, U = {n0,n1}.

(3).png

Fig. 2.10 continue, now the shortest path from n0 to n3 is n0=⇒n1=⇒n3, cost is 4, we mark n3 as visited. Now set S = {n3,n4,n5}, U = {n0,n1,n2}.

(4).png

Fig. 2.11 continue, we start to visit n3, we can update the path from n0 to n5, and the cost from n0 to n5 is 6, now the shortest path from n0 to n4 is

(17)

n0=⇒n1=⇒n2=⇒n4, cost is 4, we mark n4 as visited. Now set S = {n4,n5}, U = {n0,n1,n2,n3}.

(5).png

Fig. 2.12 continue, New cost from n0 to n4 to n5 is 7 so we don’t update the cost from n0 to n5, so we mark n5 as visited. Now set S = {n5}, U = {n0,n1,n2,n3,n4}.

(6).png

Fig. 2.13 continue, now the shortest path from n0 to n5 is n0=⇒n1=⇒n3=⇒n5, cost is 6, the shortest path is found, Now set S = {}, U = {n0,n1,n2,n3,n4,n5}, algorithm ends.

This is the description of Dijkstra’s algorithm:

step1: Mark the selected initial node n0 with a current cost of 0 and the rest with infinity.

step2: Set the non-visited node with the smallest current cost as the current node ni.

step3: For each neighbor N of your current node ni: add the current cost of ni with the weight of the edge connecting ni-N. If it’s smaller than the current cost of N, set it as the new current cost of N.

(18)

(7).png

2.3 Maude

Maude[1] is a rewriting logic-based specification and programming language equipped with model checking facilities (the Maude search command and the Maude LTL model checker)and A direct successor of OBJ3 which has many excellent functionalities:

Fast Associative-Commutative (AC) rewriting Model checking facilities

Meta-programming facilities

Which can be used in specifications of states machines that can be model checked, the search command can search all the states to see if it fits the desired property. The Maude LTL model checker verifies LTL properties of state machines.

Fig. 2.14 is the display screen of Maude.

This is an example Maude module of natural numbers: fmod NAT is

sort Nat . op 0 : ->Nat . op s : Nat ->Nat .

op + : Nat Nat ->Nat . vars N M : Nat .

eq 0 + N = N .

eq s(M) + N = s(M + N) . endfm

This module introduces a sort called Nat, and three operators, two equa-tions.

op 0 : ->Nat . means constant 0 is a natural number.

The second op s : Nat ->Nat . means s is a function which from a natural number to a natural number.

(19)

Figure 2.14: Maude display

(20)

still a natural number. The underline means we can replace it with different natural number.

vars N M : Nat . we define N M both are natural numbers.

Equation eq 0 + N = N . defines any SUM of natual number and 0 is such natural number.

Equation eq s(M) + N = s(M + N) . means the SUM of two natural number s(M) and N will be s(M + N) which is also a natural number.

Maude[5] sets out to solve a different set of problems than ordinary im-perative languages like C, Java. It is a formal reasoning tool, which can help us verify that things are ”as they should”, and show us why they are not if this is the case. Which means we can formalize some existing algorithms in to Maude language, and find some properties and do model checking.

We can use Maude search command to search all the reachable states, to look for some states that we want to.

(21)

Chapter 3 Proposed Model

3.1 Real World Situation

In the real world, there are streets and buildings. We can make the cross of the street as node, so the map of a place can be modified to some nodes and the distance between nodes. see Fig. 3.1

3.2 Formalized to Simplified Model

Then we can consider such model more simple, only nodes and the dis-tance/cost between nodes.

Fig. 3.2 Suppose there are 64 nodes in a graph, n0 is the start node, n63 is the goal, the number between nodes is the cost from one node to the other, if we want to know the shortest cost from node n0 to node n63, we should use some pathfinding algorithm such as Dijkstra.

Such model can be used to check some pathfinding algorithms like Dijk-stra’s property, but we have to formalize Dijkstra as a state machine, and then we can use some Model checker to check some properties.

(22)

(23)

(24)

Chapter 4 Model Checking of Dijkstra

4.1 Initial State and Goal

In order to model check the pathfinding algorithm such Dijkstra, we need to formalize it to a state machine. A state machine consists of initial state, state transition and states. so we need an initial state, here according to the graph, there are two neighbors of n0, and the cost from n0 to n1 is 1, the cost from n0 to n8 is 1, so we can write like this:

(node[n0]: 0,(<n1,1 ><n8,1 >),empty,n0)

Obviously, the cost from n0 to n0 is 0, so the first number is 0, <n1,1 ><n8,1 >represents the cost from node[ni] to node n1 is 1, the cost from node[n0] to node n8 is 1, empty means none of n1 and n8 is visited, the last n0 means the shortest path from n0 to node[ni], currently node[ni] is node[n0], so the shortest path is n0. There are 64 nodes in this graph, the rest of this initial state nodes will be shown in Chapter. 8

Maude is equipped with the search command that can search all the reachable states from a given state to see if enjoys the property, if we give such initial state based on the graph:

(node[n0]: 0,(<n1,1 ><n8,1 >),empty,n0) (node[n1]: oo,(<n2,2 ><n9,1 >),empty,nil) (node[n2]: oo,(<n3,1 ><n10,2 >),empty,nil) (node[n3]: oo,(<n4,1 ><n11,1 >),empty,nil) (node[n4]: oo,(<n5,1 ><n12,2 >),empty,nil) (node[n5]: oo,(<n6,2 ><n13,2 >),empty,nil) (node[n6]: oo,(<n7,2 ><n14,1 >),empty,nil) ...

(node[n60]: oo,(<n61,2 >),empty,nil) (node[n61]: oo,(<n62,2 >),empty,nil)

(25)

(node[n62]: oo,(<n63,1 >),empty,nil) (node[n63]: oo,empty,empty,nil)

For all of the initial states, we can see Chapter. 8

Now we have an initial state, the next we need is a goal, we can make a goal like this:

op goal? : NId ->Bool . var NI : NId .

eq goal?(n63) = true .

eq goal?(NI) = false [owise] .

NId is node ID, and n63 = goal is true, which means n63 is our goal.

4.2 The Pattern of Dijkstra

These figures Fig. 4.1 to Fig. 4.62 are showing the pattern of searching every nodes and finding a shortest path.

Figure 4.1: Nodes Visited 1 Figure 4.2: Nodes Visited 2

4.3 Formalizing

In order to formalize Dijkstra to state machine, some definitions are needed. This is how to achieve it step by step,

First we have to define some basic: fmod NAT+INF is

(26)

(27)

(28)

(29)

(30)

(31)

(32)

(33)

(34)

(35)

(36)

Figure 4.63: Nodes Visited 63 sorts Inf NatInf .

subsorts Nat Inf <NatInf . op oo : ->Inf [ctor] . var N : Nat . eq N <oo = true . eq oo <N = false . eq oo <oo = false . eq N >oo = false . eq oo >N = true . eq oo >oo = false . eq oo + N = oo .

(37)

eq oo + oo = oo . endfm

This is to define some basics, every natural number is smaller than infinity, infinity is equal to infinity, and the SUM of any natural number and infinity is infinity.

Then we have to define lists: fmod LIST {D :: TRIV} is sort List{D} .

subsort D$Elt <List{D} . op nil : ->List{D} [ctor] .

op -> : List{D} List{D} ->List{D} [ctor assoc id: nil] . endfm The list module is to describe the path, and connect the nodes with ”->”.

Next we have to define a module NNPAIR. fmod NNPAIR is

pr NID . pr NAT . sort NNPair .

op < , >: NId Nat ->NNPair [ctor] . endfm

This module combines natural number and node ID as a pair, which can help us to build an initial state such as <n1,1 >. Next we have to define a module SOUP:

fmod SOUP {D :: TRIV} is sort Soup{D} .

subsort D$Elt <Soup{D} . op empty : ->Soup{D} [ctor] .

op : Soup{D} Soup{D} ->Soup{D} [ctor assoc comm id: empty] . op \in : D$Elt Soup{D} ->Bool .

(38)

eq E \in empty = false . eq E \in E S = true . eq E \in S = false [owise] . endfm

Next we have to define a module NNIDLPAIR: fmod NNIDLPAIR is

pr NAT .

pr SOUP{NIdList} . sort NNIDLPair .

op < , >: Nat List{NId} ->NNIDLPair [ctor] . endfm

This module combines natural number and list of node ID together, like <1,n1->n2>.

Next we need to define a module NNIDLPSOUP: fmod NNIDLPSOUP is

pr SOUP{NNIDLPair} .

op add : Soup{NNIDLPair} NId Nat ->Soup{NNIDLPair} . op extract : Soup{NNIDLPair} ->Soup{NNIDLPair} .

op extract’ : Soup{NNIDLPair} Soup{NNIDLPair} ->Soup{NNIDLPair} . var NI : NId . vars W D D’ : Nat . vars L L’ : List{NId} . vars Ls Ls’ : Soup{NNIDLPair} . eq add(empty,NI,W) = <W,NI >.

eq add(<D,L >,NI,W) = <D + W,L ->NI >.

eq add(<D,L ><D’,L’ >Ls,NI,W) = <D + W,L ->NI >add(<D’,L’ >Ls,NI,W) .

eq extract(Ls) = extract’(Ls,empty) . eq extract’(empty,Ls’) = Ls’ .

(39)

ceq extract’(<D,L >Ls,<D’,L’ >Ls’) = extract’(Ls,<D,L >) if D <D’ .

ceq extract’(<D,L >Ls,<D’,L’ >Ls’) = extract’(Ls,<D’,L’ >Ls’) if D >D’ .

ceq extract’(<D,L >Ls,<D’,L’ >Ls’) = extract’(Ls,<D,L ><D’,L’ >Ls’) if D = D’ .

endfm

This module has three functions: add, extract, extract’: Add is built to add the cost and the path from a node to a path together, for example, there is one path n1 - >n2 and the cost is 2, the node is n3, the cost from n2 to n3 is 3, so after add, it will be n1 - >n2 - >n3, and the cost becomes 5.

Extract is to extract a Nat+Node ID List pair to itself and empty. Extract’ is to find a smallest Nat+Node ID List, which is built to find a shortest path for some nodes, for example, if we have some thing like this:

<1,n1->n2>, <2,n3->n4>, <3,n4->n5>, <4,n5->n6>

After the function Extract’, we will get only one Nat+Node ID List, which is <1,n1->n2>.

Next we need to define a module MINQUEUE: fmod MINQUEUE is

pr NNPAIR . sort MQueue .

op empq : ->MQueue [ctor] .

op | : NNPair MQueue ->MQueue [ctor] . op enq : MQueue NNPair ->MQueue . op del : MQueue NId ->MQueue . vars D D’ : Nat .

vars NI NI’ : NId . var Q : MQueue .

eq enq(empq,<NI’,D’ >) = <NI’,D’ >| empq . eq enq(<NI’,D >| Q,<NI’,D’ >)

(40)

eq enq(<NI,D >| Q,<NI’,D’ >)

= (if D’ <D then <NI’,D’ >| <NI,D >| del(Q,NI’) else <NI,D >| enq(Q,<NI’,D’ >) fi)

[owise] .

eq del(empq,NI’) = empq . eq del(<NI’,D >| Q,NI’) = Q .

eq del(<NI,D >| Q,NI’) = <NI,D >| del(Q,NI’) [owise] . endfm

There are two functions in module MINQUEUE:

Function enq is to sort the Nat+Node ID pairs based on the number of Nat from bigger to smaller, left to right.

Function deq is given a node id, delete the Nat+Node ID pair who own such node id.

Next is to define OCOMP: fmod OCOMP is pr SOUP{NNPair} . pr NNIDLPSOUP . pr MINQUEUE . pr GSTATUS . pr NAT+INF . sort OComp .

op (node[ ]: , , , ) : NId NatInf Soup{NNPair} Soup{NNPair} List{NId} ->OComp [ctor] .

op (gstat: ) : GStat ->OComp [ctor] . op (path: ) : NNIDLPair ->OComp [ctor] . op (mq: ) : MQueue ->OComp [ctor] . endfm

OCOMP means observable components, which combined node id, natural number, node id+ natural number pair, list of node id. This is built to make us observe the elements.

(41)

4.4 Rewrite Rules

After we defined what we want, we can write the rewrite rules of Dijk-stra.

The states transition of Dijkstra are specified as the following rewrite rules:

rl [fin] : (gstat: fin) OCs =⇒ (gstat: fin) OCs .

crl [goal] : (gstat: nFin) (mq: (<NI,D”’ >| Q)) (path: (<D”,L” >)) (node[NI]: D,NNPs1,NNPs2,L) OCs

=⇒ (gstat: fin) (mq: (<NI,D”’ >| Q)) (path: (<D,L >)) (node[NI]: D,NNPs1,NNPs2,L) OCs

if goal?(NI) .

Above rewrite rule is when goal is found, but when goal is not found, there will be 4 situations.

Because for a node ni, new current cost will be smaller or equal and big with current cost, and such node ni is visited or not visited, so totally there will be 4 rewrite rules like this: crl [srch1] : (gstat: nFin) (mq: (<NI,D” >| Q)) (node[NI]: D,<NI’,W >NNPs1,NNPs2,L) (node[NI’]: D’,NNPs1’,NNPs2’,L’) OCs

=⇒ (gstat: nFin) (mq: enq(<NI,D” >| Q,<NI’,D + W >)) (node[NI]: D,NNPs1,<NI’,W >NNPs2,L) (node[NI’]: D + W,NNPs1’,NNPs2’,L ->NI’) OCs

if D + W <D’ /\ NNPs1 =/= empty .

Here ”D + W” represents new current cost, ”D’” represents current cost, if NNPs1 is empty, means such node is visited, so this condition means new current cost is smaller than current cost, and such node is not been visited yet.

crl [srch2] : (gstat: nFin) (mq: (<NI,D” >| Q)) (node[NI]: D,<NI’,W >NNPs1,NNPs2,L) (node[NI’]: D’,NNPs1’,NNPs2’,L’) OCs

=⇒ (gstat: nFin) (mq: enq(Q,<NI’,D + W >)) (node[NI]: D,NNPs1,<NI’,W >NNPs2,L) (node[NI’]: D + W,NNPs1’,NNPs2’,L ->NI’) OCs

if D + W <D’ /\ NNPs1 = empty .

This condition means new current cost is smaller than current cost, and such node has been visited.

(42)

=⇒ (gstat: nFin) (mq: (<NI,D” >| Q)) (node[NI]: D,NNPs1,<NI’,W >NNPs2,L) (node[NI’]: D’,NNPs1’,NNPs2’,L’) OCs

if not (D + W <D’) /\ NNPs1 =/= empty .

This condition means new current cost is bigger or equal than current cost, and such node is not been visited yet.

crl [srch4] : (gstat: nFin) (mq: (<NI,D” >| Q)) (node[NI]: D,<NI’,W >NNPs1,NNPs2,L) (node[NI’]: D’,NNPs1’,NNPs2’,L’) OCs

=⇒ (gstat: nFin) (mq: Q) (node[NI]: D,NNPs1,<NI’,W >NNPs2,L) (node[NI’]: D’,NNPs1’,NNPs2’,L’) OCs

if not (D + W <D’) /\ NNPs1 = empty .

This condition means new current cost is bigger or equal than current cost, and such node has been visited.

we can see that if our system module is such that the set of states reachable from the initial state is finite, we can use Maude’s search command and Maude’s model checker for linear temporal logic (LTL) as decision procedures to verify some properties.

And then we can use the search command to search all reachable states. Then we can know the shortest path from the initial node n0 to goal n63:

search [1] in DIJKSTRA64 : init =⇒* (gstat: fin) OCs . Then we can get such states transition:

see Chapter. 8.

4.5 Finding all paths and model checking

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

(43)

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

(44)

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

done means 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

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

(45)

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 Two blue lines are paths found by second RL. one red line 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.

(46)

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

(47)

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.

(48)

And also true, which means the path found by Dijkstra is one of the shortest paths.

(49)

Chapter 5 More Tests

I used more graphs to do model checking these two properties.

5.1 The 2nd graph

Figure 5.1: The 2nd graph After using Dijkstra, we can find such shortest path: path: <5,n0 ->n2 ->n5 ->n3 >

After finding all paths, we can know there are 3 shortest paths in this graph.

<5,n0 ->n2 ->n5 ->n3 > <5,n0 ->n2 ->n1 ->n4 ->n3 >

(50)

<5,n0 ->n2 ->n5 ->n1 ->n4 ->n3 > After model checking, I got such result:

red in DIJKSTRA-CHECK : modelCheck(init,halt) .

Advisory: reparsing module DIJKSTRA-CHECK due to changes in im-ported modules.

Advisory: reparsing module DIJKSTRA-PREDS due to changes in im-ported modules.

reduce in DIJKSTRA-CHECK : modelCheck(init, halt) . rewrites: 477 in 0ms cpu (1ms real) (715142 rewrites/second) result Bool: true

red in DIJKSTRA-CHECK : modelCheck(init,correct) . reduce in DIJKSTRA-CHECK : modelCheck(init, correct) . rewrites: 497 in 2ms cpu (3ms real) (198800 rewrites/second) result Bool: true

Which means Dijkstra always halts, and path found by Dijkstra is one of the shortest paths.

5.2 The 3rd graph

After using Dijkstra, we can find such shortest path: <60,n1 ->n4 ->n3 ->n5 >

<60,n1 ->n4 ->n3 ->n5 >

After model checking, I got such result:

red in DIJKSTRA-CHECK : modelCheck(init,correct) . reduce in DIJKSTRA-CHECK : modelCheck(init, correct) .

(51)

Figure 5.2: The 3rd graph

5.3 The 4th graph

After using Dijkstra, we can find such shortest path: <21,n1 ->n9 ->n10 ->n11 ->n5 >

<21,n1 ->n9 ->n10 ->n11 ->n5 > After model checking, I got such result:

(52)

Figure 5.3: The 4th graph

5.4 The 5th graph

This is the graph I used in demonstrating Dijktra, let’s do model checking: After using Dijkstra, we can find such shortest path:

(53)

Figure 5.4: The 4th graph

<6,n0 ->n1 ->n3 ->n5 >

After model checking, I got such result:

(54)

Chapter 6 Discussion

6.1 Summarized diagram of the report

The diagram Fig. 6.1 shows what I have done in this research project. Real World Streets: Imagine some real-world situation.

Simple Model: To make such situation simpler by formalizing it to a graph with nodes and costs.

Some Pathfinding Algorithms Like Dijkstra: Use some pathfinding algorithms like Dijkstra.

Formalize to State Machine: To formalize Dijkstra to state machine. Model Checking: After formalizing such algorithms to state machine, use Search command to check whether such algorithm enjoys a property.

6.2 Writting with Maude code

First, we make the Maude code based on Dijkstra’ algorithm, then we can test the Maude code here is any bug or not. If we find any bug, we should check the code and rebuild it, We can modeling based on some properties such as Finite-state model extractions, Simplifications, Restrictions. Finally, we can do model checking here is an error or correct.

6.3 Model checking

The diagram Fig. 6.2 demonstrates the procedure of model checking, after testing the Maude code, we can do model checking by using search command and some properties, in this case, we use search command to search all states that whether the shortest path is found, so the counterexample is the shortest

(55)

Figure 6.1: Work done in this report

path, but if there is no conterexample is found, that means something is wrong, because obviously, this graph must have a shortest path from n0 to n63, if there is not, means no shortest path from n0 to n63, so there have to be something wrong with the Maude code, so we have to build the code again, until a counterexample is found.

(56)

(57)

Chapter 7 Conclusion

We have described the importance of pathfinding algorithms of autonomous robots/cars, and we have described state machines in a formal specification by Maude, we described state machine, invariant, Kripke structure and LTL, and then we described Dijkstra and Maude in a mathematical method, we built a model similar to the real world situation, which is easy for us to concentrate on the algorithm, and then we wrote Dijkstra’s algorithm with Maude, and we did model checking, after using a search command, we got a counterexample, which is the shortest path from the start node to the goal.

Since we got the shortest path by using Dijkstra, but we need to verify some properties of Dijkstra, so I found two properties, one is whether Dijkstra always halts, the second property is whether the path found by Dijkstra is one of the shortest paths, in order to prove these two properties, we need to know all possible path from all nodes, so I built a new model that can find all paths of each node, but when I am using the new model to find all paths in a graph which has 64 nodes, it will take a very long time, so I decrease the node number to 32, and then after about 3 minutes, it will find all possible path for all nodes, and then we need to manually find the shortest paths, there may be one or more paths which cost is the same, then we use all shortest path feed into another module to do model checking, and then we can know if Dijkstra enjoys both properties.

To prove this, I did multiple tests by using more different graphs to do model checking, after finding all paths and model checking, the results are all true, which means Dijkstra’s algorithm enjoys two properties.

There are different pathfinding algorithms nowadays, not only Dijkstra, but also other algorithms like A*, and more properties, some of the algorithm may not enjoy some properties, and we can test it after model checking, by model checking more and more pathfinding algorithms, we can prove more and more pathfinding algorithms to see whether it is trustworthy.

(58)

Bibliography

[1] May Thu Aung, Tam Thi Than Nguyen, Kazuhiro Ogata. Analysis of Two Flawed Versions of a Mutual Exclusion Protocol with Maude and SMGA, ACM, (2018)

[2] May Thu Aung, Tam Thi Than Nguyen, Kazuhiro Ogata. Guessing properties of the Qlock mutual exclustion protocol based on its graphical animations and confirming the properties by model checking, 7th In-ternational Conference on Software and Computer Applications (ICSA 2018), ACM. 2018

[3] Kazuhiro Ogata. A divide & conquer approach to liveness model check-ing under fairness & anti-fairness assumptions, Frontiers of Computer Science, 2018

[4] Kazuhiro Ogata and Kokichi Futatsugi.Specification and verifica-tion of some classical mutual exclusion algorithms with CafeOBJ, OBJ/CafeOBJ/Maude Workshop at Formal Methods 1999, 1999

[5] Manuel Clavel, Francisco Dur´an, Steven Eker, Patrick Lincoln, Narciso Mart´ı-Oliet, Jos´e Meseguer, and Carolyn Talcott. 2007. All About Maude – A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. , Lecture Notes in Computer Science (LNCS), Vol. 4350. Springer

(59)

Chapter 8 Appendix

8.1 Nodes

(node[n0]: 0,(<n1,1 ><n8,1 >),empty,n0) (node[n1]: oo,(<n2,2 ><n 9,1 >),empty,nil) (node[n2]: oo,(<n3,1 ><n10,2>),empty,nil) (node[n3]: oo,(<n4,1 ><n11,1>),empty,nil) (node[n4]: oo,(<n5,1 ><n12,2>),empty,nil) (node[n5]: oo,(<n6,2 ><n13,2>),empty,nil) (node[n6]: oo,(<n7,2 ><n14,1>),empty,nil) (node[n7]: oo,(<n15,2>),empty,nil)

(node[n8]: oo,(<n9,2 ><n16,2>),empty,nil) (node[n9]: oo,(<n10,2 ><n17,2>),empty,nil) (node[n10]: oo,(<n11,2 ><n18,1>),empty,nil) (node[n11]: oo,(<n12,2 ><n19,2>),empty,nil) (node[n12]: oo,(<n13,2 ><n20,1>),empty,nil) (node[n13]: oo,(<n14,1 ><n21,1>),empty,nil) (node[n14]: oo,(<n15,1 ><n22,2>),empty,nil) (node[n15]: oo,(<n23,1>),empty,nil)

(node[n16]: oo,(<n17,1 ><n24,1>),empty,nil) (node[n17]: oo,(<n18,1 ><n25,1>),empty,nil) (node[n18]: oo,(<n19,2 ><n26,1>),empty,nil) (node[n19]: oo,(<n20,1 ><n27,2>),empty,nil) (node[n20]: oo,(<n21,1 ><n28,2>),empty,nil) (node[n21]: oo,(<n22,1 ><n29,2>),empty,nil) (node[n22]: oo,(<n23,2 ><n30,2>),empty,nil) (node[n23]: oo,(<n31,2 >),empty,nil)

(60)

(node[n25]: oo,(<n26,2 ><n33,2>),empty,nil) (node[n26]: oo,(<n27,1 ><n34,2>),empty,nil) (node[n27]: oo,(<n28,2 ><n35,1>),empty,nil) (node[n28]: oo,(<n29,2 ><n36,1>),empty,nil) (node[n29]: oo,(<n30,1 ><n37,1>),empty,nil) (node[n30]: oo,(<n31,2 ><n38,1>),empty,nil) (node[n31]: oo,(<n39,2 >),empty,nil)

(node[n56]: oo,(<n57,2 >),empty,nil) (node[n57]: oo,(<n58,2 >),empty,nil) (node[n58]: oo,(<n59,1 >),empty,nil) (node[n59]: oo,(<n60,1 >),empty,nil) (node[n60]: oo,(<n61,2 >),empty,nil) (node[n61]: oo,(<n62,2 >),empty,nil) (node[n62]: oo,(<n63,1 >),empty,nil) (node[n63]: oo,empty,empty,nil)

(61)

8.2 Path found

Solution 1 (state 1810) OCs –>path: <17,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45 ->n53 ->n54 ->n55 ->n63 >mq: (<n63,17 >— empq) (node[n0]: 0,empty,<n1,1 ><n8,1 >,n0) (node[n1]: 1,empty,<n2,2 ><n9,1 >,n0 ->n1) (node[n2]: 3,empty,<n3,1 ><n10,2 >,n0 ->n1 ->n2) (node[n3]: 4, empty,<n4,1 ><n11,1 >,n0 ->n1 ->n2 ->n3) (node[n4]: 5,empty,<n5,1 ><n12,2 >,n0 ->n1 ->n2 ->n3 ->n4) (node[n5]: 6,empty,<n6,2 ><n13,2 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5) (node[n6]: 8,empty,<n7,2 ><n14,1 >,n0 >n1 >n2 >n3 >n4 >n5 ->n6) (node[n7]: 10,empty,<n15,2 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n7) (node[n8]: 1,empty,<n9,2 ><n16,2 >,n0 ->n8) (node[n9]: 2, empty,<n10,2 ><n17,2 >,n0 ->n1 ->n9) (node[n10]: 4,empty,<n11,2 ><n18,1 >,n0 ->n1 ->n9 ->n10) (node[n11]: 5,empty,<n12,2 ><n19,2 >,n0 ->n1 ->n2 ->n3 ->n11) ( node[n12]: 7,empty,<n13,2 ><n20,1 >,n0 ->n1 ->n2 ->n3 ->n4 ->n12) (node[n13]: 8,empty,<n14,1 ><n21,1 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13) (node[n14]: 9,empty,<n15,1 ><n22,2 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14) (node[n15]: 10,empty,<n23,1 >,n0 >n1 >n2 >n3 >n4 >n5 >n6 ->n14 ->n15) (node[n16]: 3,empty,<n17, 1 ><n24,1 >,n0 ->n8 ->n16) (node[n17]: 4,empty,<n18,1 ><n25,1 >,n0 ->n1 ->n9 ->n17) (node[n18]: 5,empty,<n19,2 ><n26,1 >,n0 ->n1 ->n9 ->n10 ->n18) (node[n19]: 7,empty,<n20,1 ><n27,2 >,n0 >n1 >n9 >n10 >n18 ->n19) (node[n20]: 8,empty,<n21,1 ><n28,2 >,n0 >n1 >n9 >n10 >n18 ->n19 ->n20) (node[n21]: 9,empty,<n22,1 ><n29,2 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n21) (node[n22]: 10,empty,<n23,2 ><n30,2 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n21 ->n22) (node[n23]: 11, empty,<n31,2 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n15 ->n23) (node[n24]: 4,empty,<n25,2 ><n32,2 >,n0 ->n8 ->n16 ->n24) (node[n25]: 5,empty,<n26,2 ><n33,2 >,n0 ->n1 ->n9 ->n17 ->n25)

(62)

(node[n26]: 6,empty,<n27,1 ><n34,2 >,n0 >n1 >n9 >n10 >n18 ->n26) (node[n27]: 7,empty,<n28,2 ><n35,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27) (node[n28]: 9,empty,<n29,2 ><n36,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n28) (node[n29]: 11,empty,<n30,1 ><n37,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n28 ->n29) (node[n30]: 12,empty,<n31,2 ><n38,1 >,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n21 ->n22 ->n30) (node[n31]: 13,empty,<n39,2 >,n0 >n1 >n2 >n3 >n4 >n5 >n6 ->n14 ->n15 ->n23 ->n31) (node[n32]: 6,empty,<n33,1 ><n40,1 >,n0 ->n8 ->n16 ->n24 ->n32) (node[n33]: 7,empty,<n34,1 ><n41,1 >,n0 >n1 >n9 >n17 >n25 ->n33) (node[n34]: 8,empty,<n35,2 ><n42,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n34) (node[n35]: 8,empty,<n36,1 ><n43,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35) (node[n36]: 9,empty,<n37,1 ><n44,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36) (node[n37]: 10,empty,<n38,2 ><n45,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n37) (node[n38]: 12,empty,<n39,1 ><n46,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n38) ( node[n39]: 13,empty,<n47,1 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n38 ->n39) (node[n40]: 7,empty,<n41,2 ><n48,2 >,n0 >n8 >n16 >n24 >n32 ->n40) (node[n41]: 8,empty,<n42,2 ><n49,2 >,n0 >n1 >n9 >n17 >n25 ->n33 ->n41) (node[n42]: 10,empty,<n43,1 ><n50,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n34 ->n42) (node[n43]: 10,empty,<n44,2 ><n51,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n43) (node[n44]: 11,empty,<n45,2 ><n52,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n44) (node[n45]: 12,empty,<n46,2 ><n53,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45) (node[n46]: 14,empty,<n47,2 ><n54,1 >,n0 >n1 >n9 >n10 >n18

(63)

-(node[n47]: 14,empty,<n55,2 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n38 ->n39 ->n47) (node[n48]: 9,empty,<n49,1 ><n56,1 >,n0 >n8 >n16 >n24 >n32 ->n40 ->n48) (node[n49]: 10,empty,<n50,2 ><n57,1 >,n0 >n1 >n9 >n17 >n25 ->n33 ->n41 ->n49) (node[n50]: 11,empty,<n51,2 ><n58,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n34 ->n42 ->n50) (node[n51]: 11,empty,<n52,2 ><n59,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n43 ->n51) (node[n52]: 13,empty,<n53,1 ><n60,1 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n44 ->n52) (node[n53]: 13,empty,<n54,1 ><n61,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45 ->n53) (node[n54]: 14,empty,<n55,1 ><n62,2 >,n0 >n1 >n9 >n10 >n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45 ->n53 ->n54) (node[n55]: 15,empty,<n63,2 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45 ->n53 ->n54 ->n55) (node[n56]: 10,empty,<n57,2 >,n0 >n8 >n16 >n24 >n32 >n40 ->n48 ->n56) (node[n57]: 11,empty,<n58,2 >,n0 ->n1 ->n9 ->n17 ->n25 ->n33 ->n41 ->n49 ->n57) (node[n58]: 12,empty,<n59,1 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n34 ->n42 ->n50 ->n58) (node[n59]: 13,empty,<n60,1 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n43 ->n51 ->n59) (node[n60]: 14,empty,<n61,2 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n44 ->n52 ->n60) (node[ n61]: 15,empty,<n62,2 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45 ->n53 ->n61) (node[n62]: 16,empty,<n63,1 >,n0 ->n1 ->n9 ->n10 ->n18 ->n26 ->n27 ->n35 ->n36 ->n37 ->n45 ->n53 ->n54 ->n62) node[n63]: 17,empty,empty,n0 >n1 >n9 >n10 >n18 >n26 >n27 ->n35 ->n36 ->n37 ->n45 ->n53 ->n54 ->n55 ->n63

This search command is searching the shortest path from node n0 to node n63, as we can see, the shortest path is found, which is

n0 >n1 >n9 >n10 >n18 >n26 >n27 >n35 >n36 >n37 >n45 ->n53 ->n54 ->n55 ->n63

(64)

8.3 All path found from the 32 nodes

(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 >) (node[n6]: done,0,empty,<n7,2 ><n14, 1 >,<8,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 >) (node[n7]: done,0,empty,<n15,2 >,<10,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n7 >) (node[n8]: done,0,empty,<n9,2 ><n16,2 >,<1,n0 ->n8 >) (node[n9]: done,0,empty,<n10,2 ><n17,2 >,<2,n0 ->n1 ->n9 ><3,n0 ->n8 ->n9 >) (node[n10]: done,0,empty,<n11,2 ><n18,1 >,<4,n0 ->n1 ->n9 ->n10 ><5,n0 ->n1 ->n2 ->n10 ><5,n0 ->n8 ->n9 ->n10 >) (node[n11]: done,0,empty,<n12, 2 ><n19,2 >,<5,n0 ->n1 ->n2 ->n3 ->n11 ><6,n0 ->n1 ->n9 ->n10 ->n11 ><7,n0 ->n1 ->n2 ->n10 ->n11 ><7,n0 ->n8 ->n9 ->n10 ->n11 >) (node[n12]: done,0,empty,<n13,2 ><n20,1 >,<7,n0 >n1 >n2 >n3 ->n4 ->n12 ><7,n0 ->n1 ->n2 ->n3 ->n11 ->n12 ><8,n0 ->n1 ->n9 ->n10 ->n11 ->n12 ><9,n0 ->n1 ->n2 ->n10 ->n11 ->n12 ><9,n0 ->n8 ->n9 ->n10 ->n11 ->n12 >) (node[n13]: done,0,empty,<n14,1 ><n21,1 >,<8,n0 >n1 >n2 >n3 ->n4 ->n5 ->n13 ><9,n0 ->n1 ->n2 ->n3 -->n4 ->n12 ->n13 ><9,n0 ->n1 >n2 >n3 >n11 >n12 >n13 ><10,n0 >n1 >n9 >n10 >n11 >n12 ->n13 ><11,n0 ->n1 ->n2 ->n10 ->n11 ->n12 -->n13 ><11,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n13 >) ( node[n14]: done,0,empty,<n15,1 ><n22,2 >,<9,n0 >n1 >n2 >n3 ->n4 ->n5 ->n6 ->n14 ><9,n0 ->n1 ->n2 ->n3 -->n4 ->n5 ->n13 ->n14 ><10,n0 ->n1 ->n2 ->n3 ->n4 ->n12 ->n13 ->n14 ><10,n0 ->n1 ->n2 >n3 >n11 >n12 >n13 >n14 ><11,n0 >n1 >n9 >n10 >n11 >n12 ->n13 ->n14 ><12,n0 ->n1 ->n2 ->n10 ->n11 ->n12 -->n13 ->n14 ><12,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n13 ->n14 >)

(node[n15]: done,0, empty,<n23,1 >,<10,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n15 ><10,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n14 ->n15 ><11,n0 ->n1 ->n2 ->n3 ->n4 ->n12 ->n13 ->n14 ->n15 ><11,n0 ->n1

(65)

>n4 ->n5 ->n6 ->n7 ->n15 ><12,n0 ->n1 ->n9 ->n10 ->n11 ->n12 ->n13 ->n14 ->n15 ><13,n0 ->n1 ->n2 ->n10 ->n11 ->n12 ->n13 ->n14 ->n15 ><13,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n13 ->n14 ->n15 >)

(node[n16]: done,0,empty,<n17,1 ><n24,1 >,<3,n0 ->n8 ->n16 >) (node[n17]: done,0, empty,<n18,1 ><n25,1 >,<4,n0 ->n1 ->n9 ->n17 ><4,n0 ->n8 ->n16 ->n17 ><5,n0 ->n8 ->n9 ->n17 >) (node[n18]: done,0,empty,<n19,2 ><n26,1 >,<5,n0 >n1 >n9 >n10 ->n18 ><5,n0 ->n1 ->n9 ->n17 -->n18 ><5,n0 ->n8 ->n16 ->n17 -->n18 ><6,n0 ->n1 ->n2 ->n10 ->n18 ><6,n0 ->n8 ->n9 ->n10 ->n18 ><6,n0 ->n8 ->n9 ->n17 ->n18 >) (node[ n19]: done,0,empty,<n20,1 ><n27,2 >,<7,n0 >n1 >n2 >n3 ->n11 ->n19 ><7,n0 ->n1 ->n9 ->n10 ->n18 ->n19 ><7,n0 ->n1 ->n9 >n17 >n18 >n19 ><7,n0 >n8 >n16 >n17 >n18 >n19 ><8,n0 >n1 ->n2 ->n10 ->n18 ->n19 ><8,n0 ->n1 ->n9 ->n10 ->n11 ->n19 ><8,n0 ->n8 ->n9 ->n10 ->n18 ->n19 ><8,n0 ->n8 ->n9 ->n17 ->n18 ->n19 ><9,n0 ->n1 ->n2 ->n10 ->n11 ->n19 ><9,n0 ->n8 ->n9 ->n10 ->n11 ->n19 >) (node[n20]: done,0,empty,<n21,1 ><n28,2 >,<8,n0 >n1 >n2 >n3 >n4 >n12 >n20 ><8,n0 >n1 >n2 >n3 >n11 >n12 >n20 ><8,n0 ->n1 ->n2 ->n3 -->n11 -->n19 ->n20 ><8,n0 -->n1 ->n9 -->n10 -->n18 -->n19 ->n20 ><8,n0 ->n1 ->n9 ->n17 ->n18 ->n19 ->n20 ><8,n0 ->n8 ->n16 ->n17 ->n18 ->n19 ->n20 ><9,n0 ->n1 ->n2 ->n10 ->n18 ->n19 ->n20 ><9,n0 ->n1 ->n9 ->n10 ->n11 ->n12 ->n20 ><9,n0 ->n1 ->n9 ->n10 ->n11 ->n19 ->n20 ><9,n0 ->n8 ->n9 ->n10 ->n18 ->n19 ->n20 ><9,n0 ->n8 ->n9 ->n17 ->n18 ->n19 ->n20 ><10, n0 ->n1 ->n2 ->n10 ->n11 ->n12 ->n20 ><10,n0 ->n1 ->n2 ->n10 ->n11 ->n19 ->n20 ><10,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n20 ><10, n0 ->n8 ->n9 ->n10 ->n11 ->n19 ->n20 >) (node[n21]: done,0,empty,<n22,1 ><n29,2 >,<9,n0 >n1 >n2 >n3 ->n4 ->n5 ->n13 ->n21 ><9, n0 ->n1 ->n2 ->n3 -->n4 ->n12 ->n20 ->n21 ><9,n0 ->n1 ->n2 ->n3 ->n11 ->n12 ->n20 ->n21 ><9,n0 ->n1 ->n2 ->n3 ->n11 ->n19 ->n20 ->n21 ><9,n0 ->n1 ->n9 ->n10 ->n18 ->n19 ->n20 ->n21 ><9,n0 ->n1 ->n9 ->n17 ->n18 ->n19 ->n20 ->n21 ><9,n0 ->n8 ->n16 ->n17 ->n18 ->n19 ->n20 ->n21 ><10,n0 ->n1 ->n2 ->n3 ->n4 ->n12 ->n13 ->n21 ><10,n0 ->n1 ->n2 ->n3 ->n11 ->n12 ->n13 ->n21 ><10,n0 ->n1 ->n2 ->n10 ->n18 ->n19 ->n20 ->n21 ><10,n0 ->n1 ->n9 >n10 >n11 >n12 >n20 >n21 ><10,n0 >n1 >n9 >n10 >n11 >n19 ->n20 ->n21 ><10,n0 ->n8 ->n9 ->n10 ->n18 ->n19 -->n20 ->n21 ><10,n0 >n8 >n9 >n17 >n18 >n19 >n20 >n21 ><11,n0 >n1 >n2 >n10 ->n11 ->n12 ->n20 ->n21 ><11,n0 ->n1 ->n2 ->n10 -->n11 ->n19 ->n20

(66)

->n9 ->n10 ->n11 ->n12 ->n20 ->n21 ><11,n0 ->n8 ->n9 ->n10 ->n11 ->n19 ->n20 ->n21 ><12,n0 ->n1 ->n2 ->n10 ->n11 ->n12 ->n13 ->n21 ><12,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n13 ->n21 >) ( node[n22]: done,0,empty,<n23,2 ><n30,2 >,<10,n0 >n1 >n2 >n3 ->n4 ->n5 ->n13 ->n21 ->n22 ><10,n0 ->n1 ->n2 ->n3 -->n4 ->n12 ->n20 ->n21 ->n22 ><10,n0 ->n1 ->n2 ->n3 ->n11 ->n12 ->n20 ->n21 ->n22 ><10,n0 ->n1 ->n2 ->n3 ->n11 ->n19 ->n20 ->n21 ->n22 ><10, n0 ->n1 ->n9 ->n10 ->n18 ->n19 ->n20 ->n21 ->n22 ><10,n0 ->n1 ->n9 ->n17 ->n18 ->n19 ->n20 ->n21 ->n22 ><10,n0 ->n8 ->n16 ->n17 ->n18 ->n19 ->n20 ->n21 ->n22 ><11,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n22 ><11,n0 >n1 >n2 >n3 >n4 >n5 >n13 >n14 >n22 ><11,n0 >n1 ->n2 ->n3 ->n4 ->n12 ->n13 -->n21 -->n22 ><11,n0 ->n1 -->n2 ->n3 ->n11 ->n12 ->n13 ->n21 ->n22 ><11,n0 ->n1 ->n2 ->n10 ->n18 ->n19 ->n20 ->n21 ->n22 ><11,n0 ->n1 ->n9 ->n10 ->n11 ->n12 ->n20 ->n21 ->n22 ><11,n0 ->n1 ->n9 ->n10 ->n11 ->n19 ->n20 ->n21 ->n22 ><11,n0 ->n8 ->n9 ->n10 ->n18 ->n19 ->n20 ->n21 ->n22 ><11,n0 ->n8 ->n9 ->n17 ->n18 ->n19 ->n20 ->n21 ->n22 ><12,n0 ->n1 ->n2 ->n3 ->n4 ->n12 >n13 >n14 >n22 ><12,n0 >n1 >n2 >n3 >n11 >n12 >n13 >n14 ->n22 ><12,n0 ->n1 ->n2 ->n10 ->n11 ->n12 ->n20 ->n21 -->n22 ><12,n0 >n1 >n2 >n10 >n11 >n19 >n20 >n21 >n22 ><12,n0 >n1 >n9 ->n10 ->n11 ->n12 ->n13 ->n21 ->n22 ><12,n0 ->n8 ->n9 -->n10 ->n11 ->n12 ->n20 ->n21 ->n22 ><12,n0 ->n8 ->n9 ->n10 ->n11 ->n19 ->n20 ->n21 ->n22 ><13,n0 ->n1 ->n2 ->n10 ->n11 ->n12 ->n13 ->n21 ->n22 ><13,n0 ->n1 ->n9 ->n10 ->n11 ->n12 ->n13 ->n14 ->n22 ><13,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n13 ->n21 ->n22 ><14,n0 ->n1 ->n2 ->n10 ->n11 ->n12 ->n13 ->n14 ->n22 ><14,n0 ->n8 ->n9 ->n10 ->n11 ->n12 ->n13 ->n14 ->n22 >) (node[n23]: done,0,empty,<n31,2 >,<11,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n15 ->n23 ><11,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n14 ->n15 ->n23 ><12,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n21 ->n22 ->n23 ><12,n0 ->n1 ->n2 ->n3 ->n4 ->n12 ->n13 ->n14 ->n15 ->n23 ><12,n0 ->n1 ->n2 ->n3 ->n4 ->n12 ->n20 ->n21 ->n22 ->n23 ><12,n0 ->n1 ->n2 >n3 >n11 >n12 >n13 >n14 >n15 >n23 ><12,n0 >n1 >n2 >n3 ->n11 ->n12 ->n20 ->n21 ->n22 ->n23 ><12,n0 ->n1 ->n2 ->n3 -->n11 ->n19 ->n20 ->n21 ->n22 ->n23 ><12,n0 ->n1 ->n9 ->n10 ->n18 ->n19 ->n20 ->n21 ->n22 ->n23 ><12,n0 ->n1 ->n9 ->n17 ->n18 ->n19 ->n20 ->n21 ->n22 ->n23 ><12,n0 ->n8 ->n16 ->n17 ->n18 ->n19 ->n20 ->n21 ->n22 ->n23 ><13,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n7 ->n15 ->n23 ><13,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n6 ->n14 ->n22 ->n23 ><13,n0 ->n1 ->n2 ->n3 ->n4 ->n5 ->n13 ->n14 ->n22 ->n23 ><13,n0 ->n1 ->n2

JAIST Repository: Investigation and Specification of Path Finding Algorithms [課題研究報告書]