# Demo2 - Pedestrian

## 1. Problem Description

This demo shows how to identify all event sequences that could result in a fault state, and see you can get ALL possible patterns only with PyUPPAAL.

1. In this demo, we validate an autonomous car algorithm in a scenario where a pedestrian crosses an intersection with traffic lights (a).
2. As depicted in (b), the interaction dynamics within the scenario can be visualized by utilizing the `UModel.get_communication_graph()` function. 
3. The pedestrian's behavior (c), including crossing times and compliance with the traffic light, is uncertain. 
4. To demonstrate the occurrence of multiple safety violations, the scenario is set up such that the car operates solely based on traffic light signals, without considering or detecting the behavior of the pedestrian.
5. Download the model: [pedestrian.xml](https://github.com/Jack0Chan/PyUPPAAL/blob/main/src/test_demos/pedestrian.xml).

<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/pedestrian_overall.png width=600 />

## 2. Construct Model, and Verify with UPPAAL Solely


```python
import pyuppaal
from pyuppaal import UModel

print(pyuppaal.__version__)
pyuppaal.set_verifyta_path(r"C:\Users\10262\Documents\GitHub\cav2024\bin\uppaal64-4.1.26\bin-Windows\verifyta.exe")


# Load the `xml` model and save as a new file in order not to overwrite current file
m = UModel("pedestrian.xml").save_as("demo_pedestrian.xml")

# enumerate all the options for verifyta.
verify_options = [' -t 0 -o 0', ' -t 0 -o 1', ' -t 1 -o 0', ' -t 1 -o 1',
                  ' -t 1 -o 3', ' -t 2 -o 0', ' -t 2 -o 1', ' -t 2 -o 3'] 
# note that '-o 2' is random, and '-o 4' is random
# UPPAAL cannot set random seed for verification, but SMC
# therefore, uncomment the following line and the results may vary
# verify_options = verify_options + [' -t 0 -o 2', ' -t 1 -o 2', ' -t 2 -o 2', ' -t 1 -o 4', ' -t 2 -o 4']

res = []

F = ["pCheckLight", "pGreen", "pRed", "pYellow", "pCrss", "cCrss"]
for i, opt in enumerate(verify_options):
    res.append(m.easy_verify(verify_options=opt).filter_by_actions(F).untime_pattern)
res = set([ "-".join(r) for r in res])
assert len(res) == 2
for trace in res:
    print(trace.split('-'))
```

    1.2.1
    ['cCrss', 'pCheckLight', 'pRed', 'pCrss']
    ['pCheckLight', 'pRed', 'pCrss', 'cCrss']
    

## 3. find_all_patterns results

Pattern 3 and 4 are new patterns that can ONLY be identified PyUPPAAL.

<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/pedestrian_patterns.png width=600 />


```python
m = UModel("pedestrian.xml").save_as("demo_pedestrian.xml")
m.queries = "E<> (PPedestrian.Crossing and PCar.Crossing)"
sigma_focus = ["pCheckLight", "pGreen", "pRed", "pYellow", "pCrss", "cCrss"]
traces = m.find_all_patterns(focused_actions=sigma_focus)
for i, trace in enumerate(traces): print(f'pattern {i+1}:', trace.untime_pattern)
assert len(traces) == 4
```

    pattern 1: ['pCheckLight', 'pRed', 'pCrss', 'cCrss']
    pattern 2: ['cCrss', 'pCheckLight', 'pRed', 'pCrss']
    pattern 3: ['pCheckLight', 'pGreen', 'pCrss', 'cCrss']
    pattern 4: ['pCheckLight', 'pYellow', 'pCrss', 'cCrss']
    

## 4. Communication Graph

Communication Graph can be generated by the coding below, and rendered by [mermaid.live](https://mermaid.live/edit#pako:eNp9kMsKwjAQRX9FZt3-QBduLLhRKOpGyWZIpm2wTcI0RaT0350-oAhiVpnLOWFyB9DeEGRQMYZ6d8uV28kpDshpqg816efJVnVM031xYyxLq-e5W7mvTIwjE7lEX8gk-k5N41-TKa_95sPCh4kPG1-QoS6yRbdqWyDOn60ggZa4RWvkS8MkK4g1taQgk6tBfipQbhQO--ivb6chi9xTAn0wGCm3KE20kJXYdJIGdA_vt5mMjZ7PS2dzdeMHujFttQ).

[![](https://mermaid.ink/img/pako:eNqFkM8KgzAMxl9FctYX8LCLwi4byLbLRi-hjVqmbaktY4jvvvgHZDBYTsnH7wvJN4K0iiCHxqNrk1spTMJVFeizTBYtyedJN23IskN181jXWi7zsHFfGjuOnsik8kIqlXfqOvuanbztN-9W3s282_mKFA3BazSbbRfY8_cqSKEn36NW_Ng4awJCSz0JyLlVVGPsggBhJkYxBnt9Gwl58JFSiE5hoFIjR9JDXmM3sOrQPKzdZ1I6WH9ew1synD5d93BC?type=jpg)](https://mermaid.live/edit#pako:eNqFkM8KgzAMxl9FctYX8LCLwi4byLbLRi-hjVqmbaktY4jvvvgHZDBYTsnH7wvJN4K0iiCHxqNrk1spTMJVFeizTBYtyedJN23IskN181jXWi7zsHFfGjuOnsik8kIqlXfqOvuanbztN-9W3s282_mKFA3BazSbbRfY8_cqSKEn36NW_Ng4awJCSz0JyLlVVGPsggBhJkYxBnt9Gwl58JFSiE5hoFIjR9JDXmM3sOrQPKzdZ1I6WH9ew1synD5d93BC)


```python
m.get_communication_graph()
```




    ```mermaid
    graph TD
    PCar--cCheckLight-->PTrafficLights
    PTrafficLights--cGreen,cRed,cYellow-->PCar
    PTrafficLights--pGreen,pRed,pYellow-->PPedestrian
    PPedestrian--pCheckLight-->PTrafficLights
    ```