KTH-SML / pyspect

Python Specification and Control with Temporal Logic Trees
MIT License
0 stars 0 forks source link

Fork hcl and odp #1

Closed kaarmu closed 11 months ago

kaarmu commented 11 months ago
kaarmu commented 11 months ago

I've managed to build hcl for Ubuntu 22 using docker. By changing base image I think it's no problem to build for whatever distribution. Checkout https://github.com/kth-sml/heterocl for instructions

kaarmu commented 11 months ago

For a T-intersection, consider a DSL that describes the regional rules like the following:

Proposition "Inside I-Lane 1 of Road 1":
    {xmin} < x < {xmax}
    {ymin} < y < {ymax}
Proposition "Inside O-Lane 1 of Road 1":
    {xmin} < x < {xmax}
    {ymin} < y < {ymax}
Proposition "Inside I-Lane 1 of Road 2":
    {xmin} < x < {xmax}
    {ymin} < y < {ymax}
Proposition "Inside Intersection 1":
    {xmin} < x < {xmax}
    {ymin} < y < {ymax}
Proposition "Facing East":
    [...]
Proposition "Facing West":
    [...]   
Proposition "Facing North":
    [...]
Proposition "Keeping Speed":
    {vmin} < v < {vmax}

Rule "Road 1, East":
    Car must be...
        * "Inside I-Lane 1 of Road 1"
        * "Facing East"
Rule "Road 1, West":
    Car must be...
        * "Inside O-Lane 1 of Road 1"
        * "Facing West"
Rule "Road 2, North":
    Car must be...
        * "Inside I-Lane 1 of Road 2"
        * "Facing North"

Rule "Road 1":
    Car must obey either...
        * "Road 1, East"
        * "Road 1, West
Rule "Road 2":
    Car must obey either...
        * "Road 2, North"
        * [...]

Rule "Region 1, Basic Rule":
    Car must...
        * keep velocity 0.1 < v < 0.9
        * and obey either...
            * "Road 1, East" 
            * "Road 1, West" 
            * "Road 2, " 
            * [...]

Rule "Go to Out 1":
    Car must when in "Port 2, North"...
        * obey "Region 1, Basic Rule"

In pyspect, with a level-set implementation, it would look something like this

# t_intersection.py

from odp.spect import *
from pyspect.rules import Proposition, And, Or
from numpy import pi

timeline = Timeline(0, 10, 0.2)
grid = Grid([ -1.2,  -1.2,  -pi,  +0.0], # min values
            [ +1.2,  +1.2,  +pi,  +1.0], # max values
            [   31,    31,   11,    11], # resolution
            [False, False, True, False]) # periodic (optional)

model = svea(ctrl_range=[[-pi/5, -0.2],
                         [+pi/5, +0.2]],
             dstb_range=[[-0.05, -0.05, -pi/20, 0],
                         [+0.05, +0.05, +pi/20, 0]],
             mode='reach')

solver = create_solver(model, grid, timeline)

facing_north = Proposition('facing_north')
facing_south = Proposition('facing_south')
facing_west = Proposition('facing_west')
facing_east = Proposition('facing_east')

ilane1_road1 = Proposition('ilane1_road1')
olane1_road1 = Proposition('ilane1_road1')
ilane1_road2 = Proposition('ilane1_road2')

road1_east = And(ilane1_road1, facing_east)
road1_west = And(olane1_road1, facing_west)
road2_north = And(ilane1_road2, facing_north)
isect1: rules.Rule

region = Or(isect1, 
            road1_east, road1_west, 
            road2_north, ...) 

# Port 1 is a goal Ego might want to reach, 
# e.g. somewhere on an O-Lane
reach_port1 = And(region, Proposition('port1'))

solver(rule=reach_port1, save_intermediary=True,
       facing_north=LevelSet(...),
       ilane1_road1=LevelSet(...),
       ...)

The level-set implementation would need to provide the following (e.g. think inside odp):

import numpy as np
from dataclasses import dataclass
from pyspect import rules 
from odp.solver import HJSolver
from dev.SVEA4D import SVEA4D

class LevelSet(rules.Set): pass

@dataclass
class Timeline: 
    start: float
    stop: float 
    resolution: float = 0.1

@dataclass
class Grid: 
    mins: list
    maxs: list
    resolution: list
    is_periodic: list = []

    def __init__(self, *args, **kwargs):
        super().__init__(*args, **kwargs)

        self.dims = len(self.mins)

        assert len(self.maxs) == self.dims
        assert len(self.resolution) == self.dims

        if self.is_periodic:
            assert len(self.is_periodic) == self.dims

def svea(ctrl_range, dstb_range, mode):
    ctrl_range = np.asarray(ctrl_range)
    dstb_range = np.asarray(dstb_range)
    assert mode in ('reach', 'avoid')

    modes = {'reach': {"uMode": "min", "dMode": "max"},
             'avoid': {"uMode": "max", "dMode": "min"}}

    return SVEA4D(uMin=ctrl_range[0, :], uMax=ctrl_range[1, :],
                  dMin=dstb_range[0, :], dMax=dstb_range[1, :],
                  **modes[mode])

def create_solver(model, grid, timeline):

    def solver(rule: rules.Rule, save_intermediary=False, **props):

        """
        make rule into value function with 
        encoded goal & constraints... The following 
        is how odp combines target and constraint

        if constraint is None:
            init_value = target
        else: 
            constraint_dim = constraint.ndim

            # Time-varying obstacle sets
            if constraint_dim > grid.dims:
                constraint_i = constraint[...,0]
            else:
                # Time-invariant obstacle set
                constraint_i = constraint

            init_value = np.maximum(target, -constraint_i)
        """
        vf: np.ndarray # created from rule & props

        # timeline to numpy
        tau: np.ndarray # created from timeline

        result = HJSolver(model, grid, vf, tau, 
                          {"TargetSetMode": "minVWithVTarget",
                           "ObstacleSetMode": "maxVWithObstacle"}, 
                          saveAllTimeSteps=save_intermediary)

        return result

    return solver
frankjjiang commented 11 months ago

The DSL is reminding me a bit of PDDL: https://www.cs.cmu.edu/afs/cs/project/jair/pub/volume20/fox03a-html/node2.html

Do I understand correctly that the DSL example you give for regional rules has no temporal operations?

t_intersection.py and the level-set implementation look good to me. Only thing to clarify on those two is in level-set implementation: the intention of create_solver() is primarily to have several generated solvers for different agents, correct?

kaarmu commented 11 months ago

That was interesting! Didn't know about PDDL...

Yes you are correct, this example has no temporal operations.

So, this example had a number of goals that I didn't write. I primarily wanted to have a "cross section" of all abstraction levels and see it sort of end-to-end.

The DSL represent some high-level human-readable representation of the specification. I wrote it as "how would I convey these rules to another human while still using a formal language". This is something the end-user would write, e.g. government-official-engineer. Then, how would that look like in "framework-specific" code, i.e. the level-set implementation. The main question here is: does the pyspect API model the problem? If the API is closely related to the DSL it reinforces that the API is good. In a perfect world there wouldn't be a need for a DSL for "normal people".

Finally, what do we need to provide in pyspect? An example from our previous discussion, how should the solver function be exposed?

I think the solver question the biggest take-away from this toy-example. In pyspect we want to set the interface for solver right? However, for the level-set implementation we need model, grid and timeline which are neither rules nor propositions. My solution here was to have a factory function that returns the actual solver function which has the interface we decided on last time.

Looking at "the cross section" like this is, IMO, a good way to concretely talk about design decisions, i.e. it's good for Tuesday when we also integrate LevelSet.