K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Alex!

Sorry for the super late reply, hopefully we can still help you out.

You have two options, either you can hack on the backend code yourself (which
might be a bit painful), or you can drive the execution from within K itself
using strategies. Basically, strategies boil down to "wrapping" the rewrite
engine with some context which allows you to do things like take snapshots of
the current state, manipulate the state, or select which rules to apply to the
state. If you want more fine-grained control, you'll have to hack on the 
backend
code yourself.

The file `domains.k` (at `k-distribution/include/builtin/domains.k`) has the
`BASIC-STRATEGY` module, which you can import. You can look at
`github.com/kframework/kat` for an example of using the strategy language to
drive symbolic execution. (Don't rely on the name `kat` being stable, we may
have to change it).

I hope this is still helpful! Let me know if you have more questions.
Everett H.

On Fri, May 19, 2017 at 06:10:54PM +0000, Alex wrote:
> Hi,
> 
> We have been using the K-framework to implement the operational semantics
> of a process algebra named Circus, which is a combination of CSP and Z.
> The current status of our work is fully reported in
> https://hal.archives-ouvertes.fr/hal-01438386
> We have now a symbolic trace generator for of a good subset of it,
> thanks to K!
> 
> By now, we are interested in guiding the trace generator.
> That means that we want to direct it in order to be sure that a given
> point of the program is reached.
> 
> Does anyone has some experience in using K for similar purpose?
> 
> Thanks for the help!