Merge branch 'main' into 3.13-fixes

BerkeleyLearnVerify · Feb 13, 2025 · 0ea15cc · 0ea15cc
2 parents 461822e + dcd0213
commit 0ea15cc
Show file tree

Hide file tree

Showing 79 changed files with 721 additions and 141 deletions.
diff --git a/.github/workflows/on-call-reminder.yml b/.github/workflows/on-call-reminder.yml
@@ -11,10 +11,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Set up Python
-        uses: actions/setup-python@v2
+        uses: actions/setup-python@v4
         with:
           python-version: '3.12'
 

diff --git a/.github/workflows/run-coverage.yml b/.github/workflows/run-coverage.yml
@@ -22,7 +22,7 @@ jobs:
     strategy:
       fail-fast: true
       matrix:
-        python-version: ["3.11"]
+        python-version: ["3.12"]
         os: [ubuntu-latest]
         extras: ["test-full"]
     runs-on: ${{ matrix.os }}

diff --git a/.github/workflows/run-simulators.yml b/.github/workflows/run-simulators.yml
@@ -10,13 +10,42 @@ jobs:
       runs-on: ubuntu-latest
       concurrency:
         group: sim
+      outputs:
+        volume_id: ${{ steps.create_volume_step.outputs.volume_id }}
+      env:
+        INSTANCE_ID: ${{ secrets.AWS_EC2_INSTANCE_ID }}
+        AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
+        AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
+        AWS_DEFAULT_REGION: ${{ secrets.AWS_REGION }}
       steps:
+        - name: Create Volume from Latest Snapshot and Attach to Instance
+          id: create_volume_step
+          run: |
+            #  Retrieve the latest snapshot ID
+            LATEST_SNAPSHOT_ID=$(aws ec2 describe-snapshots --owner-ids self --query 'Snapshots | sort_by(@, &StartTime) | [-1].SnapshotId' --output text)
+            echo "Checking availability for snapshot: $LATEST_SNAPSHOT_ID"
+
+            # Wait for the snapshot to complete
+            aws ec2 wait snapshot-completed --snapshot-ids $LATEST_SNAPSHOT_ID
+            echo "Snapshot is ready."
+
+            # Create a new volume from the latest snapshot
+            volume_id=$(aws ec2 create-volume --snapshot-id $LATEST_SNAPSHOT_ID --availability-zone us-west-1b --volume-type gp3 --size 400 --throughput 250 --query "VolumeId" --output text)
+            echo "Created volume with ID: $volume_id"
+
+            # Set volume_id as output
+            echo "volume_id=$volume_id" >> $GITHUB_OUTPUT
+            cat $GITHUB_OUTPUT
+
+            # Wait until the volume is available
+            aws ec2 wait volume-available --volume-ids $volume_id
+            echo "Volume is now available"
+
+            # Attach the volume to the instance
+            aws ec2 attach-volume --volume-id $volume_id --instance-id $INSTANCE_ID --device /dev/sda1
+            echo "Volume $volume_id attached to instance $INSTANCE_ID as /dev/sda1"
+
         - name: Start EC2 Instance
-          env:
-            INSTANCE_ID: ${{ secrets.AWS_EC2_INSTANCE_ID }}
-            AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
-            AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
-            AWS_DEFAULT_REGION: ${{ secrets.AWS_REGION }}
           run: |
             # Get the instance state
             instance_state=$(aws ec2 describe-instances --instance-ids $INSTANCE_ID | jq -r '.Reservations[].Instances[].State.Name')
@@ -27,7 +56,7 @@ jobs:
                 sleep 10
                 instance_state=$(aws ec2 describe-instances --instance-ids $INSTANCE_ID | jq -r '.Reservations[].Instances[].State.Name')
             done
-            
+
             # Check if instance state is "stopped"
             if [[ "$instance_state" == "stopped" ]]; then
                 echo "Instance is stopped, starting it..."
@@ -42,34 +71,17 @@ jobs:
                 exit 1
             fi
 
-            # wait for status checks to pass 
-            TIMEOUT=300  # Timeout in seconds
-            START_TIME=$(date +%s)
-            END_TIME=$((START_TIME + TIMEOUT))
-            while true; do
-                response=$(aws ec2 describe-instance-status --instance-ids $INSTANCE_ID)
-                system_status=$(echo "$response" | jq -r '.InstanceStatuses[0].SystemStatus.Status')
-                instance_status=$(echo "$response" | jq -r '.InstanceStatuses[0].InstanceStatus.Status')
-
-                if [[ "$system_status" == "ok" && "$instance_status" == "ok" ]]; then
-                    echo "Both SystemStatus and InstanceStatus are 'ok'"
-                    exit 0
-                fi
-
-                CURRENT_TIME=$(date +%s)
-                if [[ "$CURRENT_TIME" -ge "$END_TIME" ]]; then
-                    echo "Timeout: Both SystemStatus and InstanceStatus have not reached 'ok' state within $TIMEOUT seconds."
-                    exit 1
-                fi
-
-                sleep 10  # Check status every 10 seconds
-            done
+            # Wait for instance status checks to pass
+            echo "Waiting for instance status checks to pass..."
+            aws ec2 wait instance-status-ok --instance-ids $INSTANCE_ID
+            echo "Instance is now ready for use."
+
 
     check_simulator_version_updates:
       name: check_simulator_version_updates
       runs-on: ubuntu-latest
       needs: start_ec2_instance
-      steps: 
+      steps:
         - name: Check for Simulator Version Updates
           env:
             PRIVATE_KEY: ${{ secrets.SSH_PRIVATE_KEY }}
@@ -109,11 +121,11 @@ jobs:
                 echo "NVIDIA Driver is not set"
                 exit 1
               fi
-            '  
+            '
         - name: NVIDIA Driver is not set
           if: ${{ failure() }}
           run: |
-            echo "NVIDIA SMI is not working, please run the steps here on the instance:" 
+            echo "NVIDIA SMI is not working, please run the steps here on the instance:"
             echo "https://scenic-lang.atlassian.net/wiki/spaces/KAN/pages/2785287/Setting+Up+AWS+VM?parentProduct=JSW&initialAllowedFeatures=byline-contributors.byline-extensions.page-comments.delete.page-reactions.inline-comments.non-licensed-share&themeState=dark%253Adark%2520light%253Alight%2520spacing%253Aspacing%2520colorMode%253Alight&locale=en-US#Install-NVIDIA-Drivers"
 
     run_carla_simulators:
@@ -128,17 +140,17 @@ jobs:
             USER_NAME: ${{secrets.SSH_USERNAME}}
           run: |
             echo "$PRIVATE_KEY" > private_key && chmod 600 private_key
-            ssh -o StrictHostKeyChecking=no -i private_key ${USER_NAME}@${HOSTNAME} '
+            ssh -o StrictHostKeyChecking=no -o ServerAliveInterval=60 -o ServerAliveCountMax=3 -i private_key ${USER_NAME}@${HOSTNAME} '
               cd /home/ubuntu/actions/Scenic &&
               source venv/bin/activate &&
               carla_versions=($(find /software -maxdepth 1 -type d -name 'carla*')) &&
               for version in "${carla_versions[@]}"; do
-                echo "============================= CARLA $version ============================="  
+                echo "============================= CARLA $version ============================="
                 export CARLA_ROOT="$version"
                 pytest tests/simulators/carla
               done
             '
-            
+
     run_webots_simulators:
       name: run_webots_simulators
       runs-on: ubuntu-latest
@@ -164,39 +176,44 @@ jobs:
               done
               kill %1
             '
-      
+
     stop_ec2_instance:
       name: stop_ec2_instance
       runs-on: ubuntu-latest
-      needs: [run_carla_simulators, run_webots_simulators]
-      steps:       
+      needs: [start_ec2_instance, check_simulator_version_updates, check_nvidia_smi, run_carla_simulators, run_webots_simulators]
+      if: always()
+      env:
+        VOLUME_ID: ${{ needs.start_ec2_instance.outputs.volume_id }}
+        INSTANCE_ID: ${{ secrets.AWS_EC2_INSTANCE_ID }}
+        AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
+        AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
+        AWS_DEFAULT_REGION: ${{ secrets.AWS_REGION }}
+      steps:
         - name: Stop EC2 Instance
-          env:
-            INSTANCE_ID: ${{ secrets.AWS_EC2_INSTANCE_ID }}
-            AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }}
-            AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }}
-            AWS_DEFAULT_REGION: ${{ secrets.AWS_REGION }}
           run: |
-            # Get the instance state
+            # Get the instance state and stop it if running
             instance_state=$(aws ec2 describe-instances --instance-ids $INSTANCE_ID | jq -r '.Reservations[].Instances[].State.Name')
-
-            # If the machine is pending wait for it to fully start
-            while [ "$instance_state" == "pending" ]; do
-                echo "Instance is pending startup, waiting for it to fully start..."
-                sleep 10
-                instance_state=$(aws ec2 describe-instances --instance-ids $INSTANCE_ID | jq -r '.Reservations[].Instances[].State.Name')
-            done
-            
-            # Check if instance state is "stopped"
             if [[ "$instance_state" == "running" ]]; then
-                echo "Instance is running, stopping it..."
-                aws ec2 stop-instances --instance-ids $INSTANCE_ID
-            elif [[ "$instance_state" == "stopping" ]]; then
-                echo "Instance is stopping..."
+              echo "Instance is running, stopping it..."
+              aws ec2 stop-instances --instance-ids $INSTANCE_ID
+              aws ec2 wait instance-stopped --instance-ids $INSTANCE_ID
+              echo "Instance has stopped."
             elif [[ "$instance_state" == "stopped" ]]; then
-                echo "Instance is already stopped..."
-                exit 0
+              echo "Instance is already stopped."
             else
-                echo "Unknown instance state: $instance_state"
-                exit 1
+              echo "Unexpected instance state: $instance_state"
+              exit 1
             fi
+
+        - name: Detach Volume
+          run: |
+            # Detach the volume
+            aws ec2 detach-volume --volume-id $VOLUME_ID
+            aws ec2 wait volume-available --volume-ids $VOLUME_ID
+            echo "Volume $VOLUME_ID detached."
+
+        - name: Delete Volume
+          run: |
+            # Delete the volume after snapshot is complete
+            aws ec2 delete-volume --volume-id $VOLUME_ID
+            echo "Volume $VOLUME_ID deleted."
diff --git a/.github/workflows/run-tests.yml b/.github/workflows/run-tests.yml
@@ -34,8 +34,11 @@ jobs:
       fail-fast: true
       matrix:
         python-version: ["3.8", "3.9", "3.10", "3.11", "3.12"]
-        os: [ubuntu-latest, windows-latest]
-        extras: ["test", "test-full"]
+        os: [ubuntu-latest, windows-latest, macos-13, macos-latest]
+        include:
+          # Only run slow tests on the latest version of Python
+          - python-version: "3.12"
+            slow: true
     runs-on: ${{ matrix.os }}
 
     steps:
@@ -63,8 +66,8 @@ jobs:
 
     - name: Install Scenic and dependencies
       run: |
-        python -m pip install -e ".[${{ matrix.extras }}]"
+        python -m pip install -e ".[test-full]"
 
     - name: Run pytest
       run: |
-        pytest ${{ inputs.options || '--no-graphics' }}
+        pytest ${{ inputs.options || (matrix.slow && '--no-graphics' || '--fast --no-graphics') }}
diff --git a/docs/simulators.rst b/docs/simulators.rst
@@ -94,6 +94,8 @@ We have several interfaces to the `Webots robotics simulator <https://cyberbotic
 Our main interface provides a generic world model that can be used with any Webots world and supports dynamic scenarios.
 See the :file:`examples/webots` folder for example Scenic scenarios and Webots worlds using this interface, and `scenic.simulators.webots` for documentation.
 
+Scenic currently interfaces with Webots versions greater than or equal to 2023a.
+
 Scenic also includes more specialized world models for use with Webots:
 
 	* A general model for traffic scenarios, used in `our VerifAI paper`_.

diff --git a/examples/carla/Carla_Challenge/carlaChallenge1.scenic b/examples/carla/Carla_Challenge/carlaChallenge1.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 01.
 Control loss without previous action.
 The ego-vehicle loses control due to bad conditions on the road and it must recover, coming back to
 its original lane.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge1.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 ## SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge10.scenic b/examples/carla/Carla_Challenge/carlaChallenge10.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 10.
 Crossing negotiation at an unsignalized intersection.
 The ego-vehicle needs to negotiate with other vehicles to cross an unsignalized intersection. In
 this situation it is assumed that the first to enter the intersection has priority.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge10.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 ## SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge2.scenic b/examples/carla/Carla_Challenge/carlaChallenge2.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 02.
 Longitudinal control after leading vehicle’s brake.
 The leading vehicle decelerates suddenly due to an obstacle and the ego-vehicle must perform an
 emergency brake or an avoidance maneuver.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge2.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 ## SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge3_dynamic.scenic b/examples/carla/Carla_Challenge/carlaChallenge3_dynamic.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 03 (dynamic).
 Obstacle avoidance without prior action.
 The ego-vehicle encounters an obstacle / unexpected entity on the road and must perform an
 emergency brake or an avoidance maneuver.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge3_dynamic.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 # SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge3_static.scenic b/examples/carla/Carla_Challenge/carlaChallenge3_static.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 03 (static).
 Obstacle avoidance without prior action.
 The ego-vehicle encounters an obstacle / unexpected entity on the road and must perform an
 emergency brake or an avoidance maneuver.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge3_static.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 ## SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge4.scenic b/examples/carla/Carla_Challenge/carlaChallenge4.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 04.
 Obstacle avoidance without prior action.
 The ego-vehicle encounters an obstacle / unexpected entity on the road and must perform an
 emergency brake or an avoidance maneuver.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge4.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 ## SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge5.scenic b/examples/carla/Carla_Challenge/carlaChallenge5.scenic
@@ -1,6 +1,9 @@
 """ Scenario Description
 Based on 2019 Carla Challenge Traffic Scenario 05.
 Ego-vehicle performs a lane changing to evade a leading vehicle, which is moving too slowly.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge5.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 param map = localPath('../../../assets/maps/CARLA/Town05.xodr')
 param carla_map = 'Town05'

diff --git a/examples/carla/Carla_Challenge/carlaChallenge6.scenic b/examples/carla/Carla_Challenge/carlaChallenge6.scenic
@@ -2,6 +2,9 @@
 Based on CARLA Challenge Scenario 6: https://carlachallenge.org/challenge/nhtsa/
 Ego-vehicle must go around a blocking object
 using the opposite lane, yielding to oncoming traffic.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge6.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 # N.B. Town07 is not included with CARLA by default; see installation instructions at

diff --git a/examples/carla/Carla_Challenge/carlaChallenge7.scenic b/examples/carla/Carla_Challenge/carlaChallenge7.scenic
@@ -3,6 +3,9 @@ Based on 2019 Carla Challenge Traffic Scenario 07.
 Ego-vehicle is going straight at an intersection but a crossing vehicle 
 runs a red light, forcing the ego-vehicle to perform a collision avoidance maneuver.
 Note: The traffic light control is not implemented yet, but it will soon be. 
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge7.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 param map = localPath('../../../assets/maps/CARLA/Town05.xodr')
 param carla_map = 'Town05'

diff --git a/examples/carla/Carla_Challenge/carlaChallenge8.scenic b/examples/carla/Carla_Challenge/carlaChallenge8.scenic
@@ -3,6 +3,9 @@ Traffic Scenario 08.
 Unprotected left turn at intersection with oncoming traffic.
 The ego-vehicle is performing an unprotected left turn at an intersection, yielding to oncoming
 traffic.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge8.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 ## SET MAP AND MODEL (i.e. definitions of all referenceable vehicle types, road library, etc)

diff --git a/examples/carla/Carla_Challenge/carlaChallenge9.scenic b/examples/carla/Carla_Challenge/carlaChallenge9.scenic
@@ -1,6 +1,9 @@
 """ Scenario Description
 Based on 2019 Carla Challenge Traffic Scenario 09.
 Ego-vehicle is performing a right turn at an intersection, yielding to crossing traffic.
+
+To run this file using the Carla simulator:
+    scenic examples/carla/Carla_Challenge/carlaChallenge9.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 param map = localPath('../../../assets/maps/CARLA/Town05.xodr')
 param carla_map = 'Town05'

diff --git a/examples/carla/NHTSA_Scenarios/bypassing/bypassing_01.scenic b/examples/carla/NHTSA_Scenarios/bypassing/bypassing_01.scenic
@@ -4,6 +4,9 @@ AUTHOR: Francis Indaheng, [email protected]
 DESCRIPTION: Ego vehicle performs a lane change to bypass a slow 
 adversary vehicle before returning to its original lane.
 SOURCE: NHSTA, #16
+
+To run this file using the Carla simulator:
+    scenic examples/carla/NHTSA_Scenarios/bypassing/bypassing_01.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 #################################

diff --git a/examples/carla/NHTSA_Scenarios/bypassing/bypassing_02.scenic b/examples/carla/NHTSA_Scenarios/bypassing/bypassing_02.scenic
@@ -4,6 +4,9 @@ AUTHOR: Francis Indaheng, [email protected]
 DESCRIPTION: Adversary vehicle performs a lane change to bypass the 
 slow ego vehicle before returning to its original lane.
 SOURCE: NHSTA, #16
+
+To run this file using the Carla simulator:
+    scenic examples/carla/NHTSA_Scenarios/bypassing/bypassing_02.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 #################################

diff --git a/examples/carla/NHTSA_Scenarios/bypassing/bypassing_03.scenic b/examples/carla/NHTSA_Scenarios/bypassing/bypassing_03.scenic
@@ -6,6 +6,9 @@ adversary vehicle but cannot return to its original lane because
 the adversary accelerates. Ego vehicle must then slow down to avoid 
 collision with leading vehicle in new lane.
 SOURCE: NHSTA, #16
+
+To run this file using the Carla simulator:
+    scenic examples/carla/NHTSA_Scenarios/bypassing/bypassing_03.scenic --2d --model scenic.simulators.carla.model --simulate
 """
 
 #################################