Flowstar.jl

This package is a wrapper to Flow*, a verification tool for cyber-physical systems. Currently only continuous reachability is supported.

Direct Usage

Pass an absolute path to the *.model file to flowstar. This returns a string of the contents of the resulting *.flow file.

using Flowstar

model = download("https://home.cs.colorado.edu/~xich8622/benchmarks/laub_loomis_small.model")
flow_str = flowstar(model)

Flowstar.jl can also be used to parse the string produced by Flow* via

model = download("https://home.cs.colorado.edu/~xich8622/benchmarks/laub_loomis_small.model")
fcs = FlowstarContinuousSolution(model)

See examples/parsing.jl for additional usage.

Instead of specifying a model file directly, you can create one programatically as shown in examples/modeling.jl