Skip to content

Instantly share code, notes, and snippets.

@bennn
Last active April 17, 2021 01:45
Show Gist options
  • Save bennn/3560a21e73c36c33e53bdd3ce29ada19 to your computer and use it in GitHub Desktop.
Save bennn/3560a21e73c36c33e53bdd3ce29ada19 to your computer and use it in GitHub Desktop.
#lang forge
option problem_type temporal
// ONLY CHANGE THE VALUE OF THE myFormula PREDICATE!
// There is a control panel with lights on it. Each light has a
// different color, and over time some may be switched on or off.
abstract sig Color {}
one sig Red, Green, Blue extends Color {}
one sig Panel { var lit: set Color }
pred myFormula {
// WRITE YOUR FORMULA HERE and then run this file to test
// if your formula parses.
// - You may use: always, after, eventually, and until
// - You may NOT use: releases, ', before, historically,
// E.g.:
always { eventually { Red in Panel.lit and Green not in Panel.lit } }
}
test expect {
// This is always true!
// We're just checking that your formula is syntactically valid.
doNotChange: {myFormula or not myFormula} is sat
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment