In this page, we are going to discuss how to create scenarios for SceneChecker. An example scenario is shown below.

{
    "reachability_engine": "default",
    "refine_threshold": 10,
    "symmetry_level": "2",
    "agents": [{
        "variables": ["x", "y", "theta"],
        "mode_list": [
            ["follow_waypoint", [3, 0, 5, 0]],
            ["follow_waypoint", [5, 0, 5, 3]],
            ["follow_waypoint", [5, 3, 2, 3]],
            ["follow_waypoint", [2, 3, 2, 6]],
            ["follow_waypoint", [5, 3, 8, 3]],
            ["follow_waypoint", [8, 3, 8, 0]]
        ],
        "edge_list": [[0,1],[1,2],[2,3],[1,4],[4,5]],
        "guards": [
            ["Box", [[4.6, -0.4, -6.28], [5.4, 0.4, 6.28]]],
            ["Box", [[4.6, 2.6, -6.28], [5.4, 3.4, 6.28]]],
            ["Box", [[1.6, 2.6, -6.28], [2.4, 3.4, 6.28]]],
            ["Box", [[4.6, 2.6, -6.28], [5.4, 3.4, 6.28]]],
            ["Box", [[7.6, 2.6, -6.28], [8.4, 3.4, 6.28]]]
        ],
        "initialSet": ["Box", [[2.2, -0.3, -0.1], [2.8, 0.3, 0.1]]]
        "initialModeID": 0,
        "segLength": -1,
        "timeHorizons": [2,3,3,3,3,3],
        "directory": "examples/models/NN_car_TR_noNN",
    }],
    "time_step": 0.01,
    "unsafeSet": [
        ["Box",[[-1,2,-100],[1.8,6,100]]]
    ]
}

The visualization of the scenario is shown below.

The components in the scenario is shown as following.

• The “reachability_engine” entry in the scenario file specify the reachability subroutine used compute the reachtube. The available reachtube subroutine now are “default” for DryVR and “flowstar” for Flow*.

"reachability_engine": "default",

• The “refine_threshold” entry in the scenario file specify the max number of refinement that can happen.

"refine_threshold": 10,

• The “symmetry_level” entry in the scenario file specify the type of symmetry used while verify the scenario. “0” is for not using any symmetry, “1” is for using only translation symmetry and “2” is for using both translation and rotation symmetry.

"symmetry_level": "2",

• The “agent” entry in the scenario file specify the plan of the agent in the scenario.

    
"agents": [{
    "variables": ["x", "y", "theta"],
    "mode_list": [
        ["follow_waypoint", [3, 0, 5, 0]],
        ["follow_waypoint", [5, 0, 5, 3]],
        ["follow_waypoint", [5, 3, 2, 3]],
        ["follow_waypoint", [2, 3, 2, 6]],
        ["follow_waypoint", [5, 3, 8, 3]],
        ["follow_waypoint", [8, 3, 8, 0]]
    ],
    "edge_list": [[0,1],[1,2],[2,3],[1,4],[4,5]],
    "guards": [
        ["Box", [[4.6, -0.4, -6.28], [5.4, 0.4, 6.28]]],
        ["Box", [[4.6, 2.6, -6.28], [5.4, 3.4, 6.28]]],
        ["Box", [[1.6, 2.6, -6.28], [2.4, 3.4, 6.28]]],
        ["Box", [[4.6, 2.6, -6.28], [5.4, 3.4, 6.28]]],
        ["Box", [[7.6, 2.6, -6.28], [8.4, 3.4, 6.28]]]
    ],
    "initialSet": ["Box", [[2.2, -0.3, -0.1], [2.8, 0.3, 0.1]]]
    "initialModeID": 0,
    "segLength": -1,
    "timeHorizons": [2,3,3,3,3,3],
    "directory": "examples/models/NN_car_TR_noNN",
}],

• The “variables” entry in the scenario file specify the variables to be verified for the agent.

"variables": ["x", "y", "theta"],

• The “mode_list” entry in the scenario file specify the list of segments that the agent is following.

"mode_list": [
    ["follow_waypoint", [3, 0, 5, 0]],
    ["follow_waypoint", [5, 0, 5, 3]],
    ["follow_waypoint", [5, 3, 2, 3]],
    ["follow_waypoint", [2, 3, 2, 6]],
    ["follow_waypoint", [5, 3, 8, 3]],
    ["follow_waypoint", [8, 3, 8, 0]]
],

• The “edge_list” entry in the scenario file specify the possible transits between different segments.

"edge_list": [[0,1],[1,2],[2,3],[1,4],[4,5]],

• The “guards” entry in the scenario file defines the set of states at which a mode transition over an edge is possible.

"edge_list": [[0,1],[1,2],[2,3],[1,4],[4,5]],

• The “initialSet” and “initialModeID” entry in the scenario file specify set of possible initial states and the initial segment the agent is following.

"initialSet": ["Box", [[2.2, -0.3, -0.1], [2.8, 0.3, 0.1]]],
"initialModeID": 0,

• SceneChecker is able to split longer segment in the plan to shorter ones with equal length to better utilize symmetry. The “segLength” entry in the scenario file specify the maximum segment length for the shorter segment. When the value is set to -1, the original plan will not be splitted.

"segLength": -1,

• The “timeHorizons” entry in the scenario file specify the list of time bounds for each modes.

"timeHorizons": [2,3,3,3,3,3],

• The “directory” entry in the scenario file dynamics file that corresponds to the agent.

"directory": "examples/models/NN_car_TR_noNN",

• The “time_step” entry in the scenario file specify the simulation time step for the reachability subroutine.

"time_step": 0.01,

• The “unsafeSet” entry in the scenario file specify the list of obstacles in the scenario. The obstacles in the scenarios can either be specified by
  • “Box”, a hyper-rectangle specified by its upper and lower bound on each dimension.
  • “Vertices”, a polytope specified by vertices.
  • “Matrix”, the A and b matrix defining the polytope as {x|Ax ≤ b}.

The obstacle in this example is specified by “Box”.

"unsafeSet": [
    ["Box",[[-1,2,-100],[1.8,6,100]]]
]