diff --git a/docs/source/figs/both.png b/docs/source/figs/both.png
new file mode 100644
index 00000000..beae42f4
Binary files /dev/null and b/docs/source/figs/both.png differ
diff --git a/docs/source/figs/console.png b/docs/source/figs/console.png
index fff875e3..a6854076 100644
Binary files a/docs/source/figs/console.png and b/docs/source/figs/console.png differ
diff --git a/docs/source/figs/full.png b/docs/source/figs/full.png
new file mode 100644
index 00000000..5d4815cc
Binary files /dev/null and b/docs/source/figs/full.png differ
diff --git a/docs/source/figs/partial.png b/docs/source/figs/partial.png
new file mode 100644
index 00000000..ba0eb01d
Binary files /dev/null and b/docs/source/figs/partial.png differ
diff --git a/docs/source/figs/rect1.png b/docs/source/figs/rect1.png
deleted file mode 100644
index ba0eb44d..00000000
Binary files a/docs/source/figs/rect1.png and /dev/null differ
diff --git a/docs/source/figs/rect2.png b/docs/source/figs/rect2.png
index b05d7c17..d02aeca7 100644
Binary files a/docs/source/figs/rect2.png and b/docs/source/figs/rect2.png differ
diff --git a/docs/source/figs/refine.png b/docs/source/figs/refine.png
new file mode 100644
index 00000000..c5acc746
Binary files /dev/null and b/docs/source/figs/refine.png differ
diff --git a/docs/source/figs/vehicle1.png b/docs/source/figs/vehicle1.png
index 0ce2e19f..9dc032be 100644
Binary files a/docs/source/figs/vehicle1.png and b/docs/source/figs/vehicle1.png differ
diff --git a/docs/source/figs/vehicle2.png b/docs/source/figs/vehicle2.png
new file mode 100644
index 00000000..46b13e6a
Binary files /dev/null and b/docs/source/figs/vehicle2.png differ
diff --git a/docs/source/troubleshooting.md b/docs/source/troubleshooting.md
index 8c08765d..1584a5ce 100644
--- a/docs/source/troubleshooting.md
+++ b/docs/source/troubleshooting.md
@@ -21,6 +21,7 @@ Verse's parser only supports the following:
This means that the following are *not* supported in reachability (don't even try it):
- print statements
- numpy functions
+- variables defined behind an if statement
- loops (except any and all statements)
@@ -42,27 +43,23 @@ if ego.craft_mode == CraftMode.Normal:
```
-## Interpreting the Console Output
+## Interpreting the Console Output
-Remember that Verse builds a tree of nodes everytime a mode transition needs to happen.
+Verse builds a tree where each node stores the trace/reachable set after each mode transition.
-Whenever a transition is evaluated, a console message will appear.
+Whenever a transition has occured, a console message will appear.
The node number is the id of the node in order of when it was first added to the processing queue.
-The "start:" indicates the time that this transition occured. If this number is not changing, then an infinite loop has occured.
+The "Time:" indicates the time that this transition occured. If this number is not changing, then an infinite loop has occured.
On the next line, it will display each agent and the mode of that agent after the transition. If an infinite loop occurs, you can look at this line to see which modes are being looped through.
-Ignore the array of numbers
-
-
+If there is another mode transition at this point, it will print the condition of the DL that triggered this transition.
## Resolving Infinite Loops
-**At each timestep, each if statement will be checked. All if conditions marked as true will be evaluated.**
-
Take this decision logic snippet:
```python
@@ -74,7 +71,7 @@ if ego.craft_mode == CraftMode.Normal:
next.craft_mode == CraftMode.Down
```
-We can see that the transition condition is the exact same in both if statements. In this case, both the "up" and "down" branches will both be ran by Verse.
+We can see that the transition condition is the exact same in both if statements. In this case, both the "up" and "down" branches will both be ran by Verse. This is how Verse handles non-determinism and this will not cause an infinite loop
Now take, for example, this logic:
@@ -89,86 +86,97 @@ if ego.craft_mode == CraftMode.Up:
```
+In Verse, a transition can happen IMMEDIATELY before time continues
-In this example, we can clearly see a cycle. Think about how the program will run timestep by timestep. When the craft mode is "Normal", it will transition to "Up" due to the 1st if statement. Then in the next timestep, the craft will transition to "Normal" due to the 2nd if condition. In the next timestep, the craft will transition to "Up" again due to the 1st if statement. Avoid situations where a mode transition can occur too soon. This includes "self-loops" where a mode transitions to itself.
-
+In this example, we can clearly see a cycle. When the craft mode is "Normal", it will transition to "Up" due to the 1st if statement. Then it will IMMEDIATELY transition back to Normal due to the 2nd condition being true.
+Avoid situations where a transition can happen immediately after another.
-To fix this problem, make the transition condition more specific:
+
+Another example:
```python
-if ego.craft_mode == CraftMode.Normal and ego.z <= 50:
+if ego.z <= 50:
next.craft_mode == CraftMode.Up
-if ego.craft_mode == CraftMode.Up and ego.z > 70:
- next.craft_mode == CraftMode.Normal
-
```
-In this scenario, let's assume that z is a state variable that is increasing in the "Up" tactical mode. Now, the transition condition for the first branch (z <= 50) does not overlap with the second branch (z > 50). There is no longer any chance of a cycle occuring.
+In this case, this if statement will be evaluated but before time can coninue, the same transition will IMMEDIATELY happen again.
+This is because ego.z has not changed since time has not continued forward.
+
+Make the transition condition more specific to include the mode in the if statement:
-Another example:
```python
-if ego.z <= 50:
+if ego.craft_mode == CraftMode.Normal and ego.z <= 50:
next.craft_mode == CraftMode.Up
```
-In this case, this if statement will be evaluated consecutively between timesteps as long as ego.z <= 50. Verse will keep trying a transition to "Up" and will appear like an infinite loop. This is because at each timestep, Verse will check all if branches to and analyze all branches that are 'true.'
+if you are still having an infinite loop consider this example:
-Again, make the transition condition more specific:
```python
-if ego.craft_mode == CraftMode.Normal and ego.z <= 50:
- next.craft_mode == CraftMode.Up
+if ego.x < 40 and ego.mode != N:
+ next.mode = N
-```
+if ego.x > 50 and ego.mode != M:
+ next.mode = M
-if you are still having an infinite loop consider this example:
+```
-The vehicle is in normal mode and is moving to the left. If it passes the red boundary, it will transition. If it passes the blue boundary, it will transition to the original mode.
+Vehicle state is single point with negative velocity and mode M. This means it is moving to the left.
+The colored regions (loosely) represent the guard/transition region where a transition can happen
-
-Verse over-approximates the reachable set for the car as a rectangle.
+
-
+Verify function over-approximates state as a rectangle (slice of reachable set )
-If this rectangle is too big, it may cross both boundaries at the same time. As you can probably imagine, if both conditions are met at the same time, then there may be a loop since VERSE will try to run both transitions at the same time.
-If you do not see a cycle in your logic and there is still an infinite loop, you may need to make the transition conditions further apart or restructure the logic.
-Take this example:
-```python
+When Entering guard region, Rectangle will first PARTIALLY intersect guard until it is FULLY contained in guard region.
-if ego.craft_mode == CraftMode.Normal and ego.x <= 30:
- next.craft_mode == CraftMode.Accel
-if ego.craft_mode == CraftMode.Accel and ego.x > 30:
- next.craft_mode == CraftMode.Normal
-
+Partially intersecting:
+
-```
-Here the the transition boundary is x = 30 for both transitions. The distance between these boundaries needs to be increased:
+Full Containment
+
+
+When the rectangle is PARTIALLY intersecting two or more guard regions, this will cause an infinite loop as Verse will again try to repeatedly analyze all possible transitions
+
+
+
+Solution:
+
+Make guard region boundaries further apart
+
+
```python
-if ego.craft_mode == CraftMode.Normal and ego.x <= 30:
- next.craft_mode == CraftMode.Accel
-if ego.craft_mode == CraftMode.Accel and ego.x > 45:
- next.craft_mode == CraftMode.Normal
-
+if ego.x < 30 and ego.mode != N:
+ next.mode = N
+
+if ego.x > 50 and ego.mode != M:
+ next.mode = M
```
+OR, use verify_refine() function which will repeatedly partition the initial set into smaller and smaller chunks until all of the initial set is safe.
+
+
+
+When the initial set is smaller, verse's over-aproximation tends to be smaller as well.
+
+
+
-If you are doing the 484 MP, you may also use verify_refine which will not cause an infinite loop this way. However, this will take much longer. Verify_refine will repeatedly call verify on partitions of the initial set. It starts by partitioning into larger regions, then get progressively gets smaller if those larger partitions are unsafe or cause an infinite loop. When the initial set is partitioned into smaller regions, the rectangles/reachable set created will eventually get small enough to fit between transition regions. Please note that verify_refine will not help if there is a cycle in your logic.
-**When running verify_refine, please let it run to the very end and ignore any intermediate console output**
## Other Issues