Idea: offline monitoring

[ivanperez-keera]

So, Copilot is capable of doing offline monitoring, but we never really made it ergnomic.

I thought of a possible starting point:

If you have a data type to hold concrete samples from externs in a given spec:

data StructData = StructData
  { myExternStream1 :: [Int8]
  , myExternStream2 :: [Int8]
  , myExternStream3 :: [Array 2 (Int 8)]
  }

a function to read that data from a file:

readInputData :: FilePath -> IO (Either String StructData)

and a function to inject the data into an existing Spec:

-- | Replace the samples in extern streams with data in a `StructData`
overwriteStreams :: Core.Spec -> StructData -> Core.Spec

then we could compose that easily and use the interpreter to check a property.

I imagine there may be a way to make that struct heterogeneous so that values of different types could be read from a file. The overwriteStreams function in that case might report additional information, such as an extern in the StructData not matching the type of the same extern in the Spec, or an extern not having as much data as others.

I thought I'd put it here in case someone wants to play with this idea.