shortestpathwithconstraint.idp

//The time complexity for this algorithm is O(n3) where n is the number of nodes.
//Vocabulary for the program
vocabulary V {
type node
beg :node
end : node
edge(node,node)
edgeOnPath(node,node)
reaches(node,node)
}

//Theory for the program
theory T : V {
{!x y :  reaches(x ,y)<-edgeOnPath ( x , y ) .
 !x y z : reaches(x,y) <- reaches ( x , z ) & reaches ( z , y ) . }

! x [ node ] y [ node ] : edgeOnPath ( x , y ) => edge ( x , y ) . // ( 1 )
reaches (beg ,end) . // ( 2 )
~(? x : edgeOnPath ( x , beg)) & ~(? x : edgeOnPath ( end , x ) ) . // ( 3 )

! x : (?<2 y : edgeOnPath ( y , x ) ) &
(?<2 y : edgeOnPath ( x , y ) ) . // ( 4 )
! x y : edgeOnPath ( x , y ) => reaches ( beg , y ) . // ( 5 )
}

//Structure defining the input of the program
structure S : V {
node = {A;B;C;D;E;F;G;H;I;J;K;L;M;N;O;P;Q;R;S;T;U;V;W;X;Y;Z} 
edge = {('T', 'Q'); ('L', 'Q'); ('D', 'F'); ('N', 'B'); ('N', 'S'); ('J', 'B'); ('H', 'O'); ('C', 'F'); ('N', 'A');('N', 'O'); ('Q', 'E'); ('Z', 'H'); ('W', 'Y'); ('P', 'T'); ('F', 'J'); ('S', 'F'); ('C', 'V'); ('D', 'P'); ('D', 'F'); ('W', 'F')} // 
beg=T
end=E
}
//Term for the program which defines the lengthOfPath
term lengthOfPath : V { #{ x y : edgeOnPath ( x , y ) } }

//Main procedure for the program
procedure main(){
//Calculate the shortest path aggregate of tuples in the shortest path
shortestPath=minimize(T,S,lengthOfPath)[1]
//if shortest path is null
if ( shortestPath == nil )
then print ("No models exist . \ n " ) 
else print(shortestPath )
end
}