Scenario

In Verse, a scenario represents a certain environment in which verification experiments can happen, and thus would be the main object for interaction. As mentioned in Creating Scenario in Verse, a scenario mainly consists of 3 components:

  1. Agents which can interact with one another,

  2. A map in which these agents interact, and defines apart of the dynamics of these agents, and

  3. A sensor that controls how the state information of agents will be shared.

When no sensor is explicitly supplied, the default sensor will be used, which simply exposes all state information of all agents as-is to all agents.

In addition to these components, a scenario can be configured using a ScenarioConfig object, which controls the simulation and verification behaviors.

ScenarioConfig([incremental, ...])

Configuration for how simulation/verification is performed for a scenario.

Scenario.add_agent(agent)

Adds an agent to the scenario.

Scenario.set_init_single(agent_id, init, ...)

Sets the initial conditions for a single agent.

Scenario.set_init(init_list, init_mode_list)

Sets the initial conditions for all agents.

Scenario.set_sensor(sensor)

Sets the sensor for the scenario.

Scenario.set_map(track_map)

Sets the map for the scenario.

Simulation & Reachability Analysis

Once a scenario is created, the user can perform simulation and verification in the scenario. This is done by calling either the .simulate() or .verify() methods. The common parameters for both methods are:

  • time_horizon: The length of time to run the simulation/reachability analysis for, in seconds.

  • time_step: The length of time between discrete transitions are checked, in seconds. This is also the time resolution at which trajectories are recorded. As the time_step gets smaller, the analysis will get more accurate, but also take more time to finish.

  • max_height: The height at which the analysis will stop for a particular branch/path.

Scenario.simulate(time_horizon, time_step[, ...])

Computes a single simulation trace of a scenario, starting from a single initial state.

Scenario.verify(time_horizon, time_step[, ...])

Compute the set of reachable states, starting from a set of initial states states.

Both methods produce traces of type AnalysisTree. An AnalysisTree stores the segments of trajectories a scenario produced, represented by an AnalysisTreeNode. A new node or trajectory segment is generated as the mode of the system changes. Note that as a system may have non-deterministic transitions, hence why the resulting reachset is a tree.

AnalysisTree(root)

A tree containing the reachable states the scenario produced.

AnalysisTreeNode(trace, init, mode, static, ...)

A AnalysisTreeNode stores the continous execution of the system without transition happening