Skip to content

Commit

Permalink
Added ContractResult Class.
Browse files Browse the repository at this point in the history
  • Loading branch information
Eric-Vin committed Nov 28, 2023
1 parent c6930a1 commit 76ef597
Show file tree
Hide file tree
Showing 6 changed files with 52 additions and 8 deletions.
2 changes: 1 addition & 1 deletion examples/contracts/compile.py
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,6 @@

filename = Path(os.path.dirname(os.path.realpath(__file__))) / "dev.contract"
scenic_ast = parse_file(filename)
python_ast, _ = compileScenicAST(scenic_ast)
python_ast, _ = compileScenicAST(scenic_ast, filename=filename)
print(ast.unparse(python_ast))
exec(compile(python_ast, filename, "exec"))
25 changes: 25 additions & 0 deletions src/scenic/contracts/contracts.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,28 @@ def __init__(self, **kwargs):

# TODO: Handle contracts w/ more than one object
assert len(self.objects) <= 1


class ContractResult:
def __init__(self, assumptions, guarantees, evidence):
self.assumptions = assumptions
self.guarantees = guarantees
self.evidence = evidence

def __str__(self):
string = "ContractResult:\n" " Assumptions:\n"

for a in self.assumptions:
string += f" {a}\n"

string += " Guarantees:\n"

for g in self.guarantees:
string += f" {g}\n"

string += f" Evidence: {self.evidence}\n"
return string


class ContractEvidence:
pass
16 changes: 12 additions & 4 deletions src/scenic/contracts/testing.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
import rv_ltl
import scipy

from scenic.contracts.contracts import ContractEvidence, ContractResult
from scenic.contracts.utils import linkSetBehavior, lookuplinkedObject
from scenic.core.distributions import RejectionException
from scenic.core.dynamics import GuardViolation, RejectSimulationException
Expand Down Expand Up @@ -69,8 +70,15 @@ def verify(self):
print(f" {cond} = {cond.check(self.evidence)}")

# Check requirements
self.evidence.requirementsMet = all(
cond.check(self.evidence) for cond in self.reqConditions
)

return self.evidence
# Package contract result and return
result = ContractResult(
self.contract.assumptions, self.contract.guarantees, self.evidence
)
return result

def runTests(self, num_tests):
# Generate scenes
Expand Down Expand Up @@ -230,11 +238,11 @@ def __init__(self, result, scene_bytes, sim_replay, start_time):
self.sim_replay = sim_replay


class ProbabilisticEvidence:
class ProbabilisticEvidence(ContractEvidence):
def __init__(self, confidence):
self.confidence = confidence
self.testData = []
self.requirements_met = None
self.requirementsMet = None

# Initialize metrics
self.elapsed_time = 0
Expand Down Expand Up @@ -281,7 +289,7 @@ def __iter__(self):
return self.testData

def __str__(self):
return f"Probabilistic Evidence: {100*self.correctness:.2f}% Correctness with {100*self.confidence:.2f}% Confidence"
return f"Probabilistic ({100*self.correctness:.2f}% Correctness with {100*self.confidence:.2f}% Confidence)"


## Termination/Requirement Conditions
Expand Down
6 changes: 5 additions & 1 deletion src/scenic/core/propositions.py
Original file line number Diff line number Diff line change
Expand Up @@ -102,13 +102,17 @@ def has_temporal_operator(self):


class Atomic(PropositionNode):
def __init__(self, closure, syntax_id):
def __init__(self, closure, syntax_id, source=None):
ap = rv_ltl.Atomic(identifier=str(syntax_id))
super().__init__(ap)
self.syntax_id = syntax_id
self.closure = closure
self.source = source

def __str__(self):
if self.source:
return f"({self.source})"

return (
f"(AP syntax_id={self.syntax_id})" if self.syntax_id is not None else "(AP)"
)
Expand Down
7 changes: 7 additions & 0 deletions src/scenic/syntax/compiler.py
Original file line number Diff line number Diff line change
Expand Up @@ -320,11 +320,18 @@ def _create_atomic_proposition_factory(self, node):
syntaxIdConst = ast.Constant(syntaxId)
ast.copy_location(syntaxIdConst, node)

try:
with open(self.filename, mode="r") as file:
source_segment = ast.get_source_segment(file.read(), node)
except FileNotFoundError:
source_segment = None

ap = ast.Call(
func=ast.Name(id=ATOMIC_PROPOSITION, ctx=loadCtx),
args=[closure],
keywords=[
ast.keyword(arg="syntaxId", value=syntaxIdConst),
ast.keyword(arg="source", value=ast.Constant(source_segment)),
],
)
ast.copy_location(ap, node)
Expand Down
4 changes: 2 additions & 2 deletions src/scenic/syntax/veneer.py
Original file line number Diff line number Diff line change
Expand Up @@ -2103,8 +2103,8 @@ def range(*args):
### Temporal Operators Factories


def AtomicProposition(closure, syntaxId):
return propositions.Atomic(closure, syntaxId)
def AtomicProposition(closure, syntaxId, source=None):
return propositions.Atomic(closure, syntaxId, source)


def PropositionAnd(reqs):
Expand Down

0 comments on commit 76ef597

Please sign in to comment.