flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Expose public API to sort checking #147

Closed wilcoxjay closed 1 year ago

wilcoxjay commented 1 year ago

This PR cleans up the sort checker and introduces a public API for sort checking individual terms in a scope.

Here's a little example:

let sig = parse_signature(
    "
    sort round
    immutable le(round, round): bool
    ",
);
let mut ctx = Scope::new(&sig).expect("could not create context");
ctx.add_variable("r", &Sort::Id("round".to_owned()))
    .expect("could not add x to the scope");
let sort = ctx
    .sort_check_term(&mut parser::term("le(r,r)"))
    .expect("unexpected sort checking error");
assert_eq!(sort, Sort::Bool);
vmwclabot commented 1 year ago

@wilcoxjay, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding Signed-off-by: John Doe <john.doe@email.org> to the last line of each Git commit message. The e-mail address used to sign must match the e-mail address of the Git author. Click here to view the Developer Certificate of Origin agreement.

wilcoxjay commented 1 year ago

Thanks, I fixed the merge conflicts. I believe @odedp wanted to look at this interface to see if it would work for him, but we can do that after merge. I'd rather get the PR queue down now.