# ParaPlan: a tool for parallel reachablity analysis of planar polygonal differential inclusion systems

Based on the papers and previous work of Gordon J. Pace, Gerardo Schneider and others: http://www.cs.um.edu.mt/~svrg/Tools/SPeeDI/index.html

How to build it: install SFML for drawer and just type "make" in each directory.

## solver

Solves a reachability task on SPDI. Given a set *S* of start edge intervals and a set *F* of final edge intervals, tests whether there exist a trajectory starting in *S* and ending in *F*.

parameters: .spdi file, .task file

## generator

Generates random SPDI by convex polygonal partitioning of a plane based on Voronoi diagrams. Number of center points in diagram is a parameter. After generation, some regions are pruned if some of their vertices are out of bounds (between 0 and 1000 along each coordinate).

Each edge in SPDI could be an output edge for at most one region (otherwise, there will be a Zeno behavior). Hence, to define a differential inclusion on a given partition, one can assign a set of (sequential) output edges for each region and test that the oriented angle between the pre-leftmost and the post-rightmost edges is positive. If all output edges are correctly set, one can assign two vectors to each region by taking it randomly between the pre-leftmost and post-rightmost edge vectors.

Vectors are assigned to each region as following:

```
Randomly iterate by all regions
with region R:
   find all starting edges E (free edge with non-free previous neighbour)
   
   if E is empty
       if no free edges in R
           return FAILURE
       else // all edges are free, no edge with non-free neighbour
           E = {random edge from R}

   with each starting edge E:
       try to take sequence of free edges starting from E, so that it could define an output set for R
   if no output set is obtained
       return FAILURE
   else
       assign two random vectors between pre-leftmost and post-righmost edge to R
```

If all regions are correctly assigned, an SPDI representation is printed on output, otherwise, nothing is printed.

parameters: number of initial region centers in Voronoi diagram (output SPDI could contain less number of regions, but not more)

## task_generator

Generates random reachability task for given SPDI, taking one random interval of one random edge as a starting set and one random interval of one random edge as a final set.

parameters: .spdi file

## draw

Draws given SPDI file on a plane, with coordinates normalization on SCREEN_HEIGHT and SCREEN_WIDTH constants (hardcoded).

paramters: .spdi file