copilot-core-3.2.1: An intermediate representation for Copilot.
Safe HaskellSafe
LanguageHaskell2010

Copilot.Core.Interpret.Eval

Description

A tagless interpreter for Copilot specifications.

Synopsis

Documentation

type Env nm = [(nm, Dynamic)] Source #

An environment that contains an association between (stream or extern) names and their values.

type Output = String Source #

The simulation output is defined as a string. Different backends may choose to format their results differently.

data ExecTrace Source #

An execution trace, containing the traces associated to each individual monitor trigger and observer.

Constructors

ExecTrace 

Fields

  • interpTriggers :: [(String, [Maybe [Output]])]

    Map from trigger names to their optional output, which is a list of strings representing their values. The output may be Nothing if the guard for the trigger was false. The order is important, since we compare the arg lists between the interpreter and backends.

  • interpObservers :: [(String, [Output])]

    Map from observer names to their outputs.

Instances

Instances details
Show ExecTrace Source # 
Instance details

Defined in Copilot.Core.Interpret.Eval

eval Source #

Arguments

:: ShowType

Show booleans as 0/1 (C) or True/False (Haskell).

-> Int

Number of steps to evaluate.

-> Spec

Specification to evaluate.

-> ExecTrace 

Evaluate a specification for a number of steps.