cs1710-ltl-template.rkt

#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
}