cs1710-roboTrain

roboTrain.frg

#lang forge
option problem_type temporal

// ONLY CHANGE THE VALUE OF THE myFormula PREDICATE!

// There is a robotic train with three components: an engine, a door, and
// a headlight.
// At any point in time:
// - the Engine may be on or off
// - the Door may be on (open) or off (closed)
// - the Light may be on or off
abstract sig Component {}
one sig Engine, Door, Light extends Component {}
one sig Train { var on: set Component }

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 { Engine in Train.on and Door not in Train.on } }
}

test expect {
    // This is always true!
    // We're just checking that your formula is syntactically valid.
    doNotChange: {myFormula or not myFormula} is sat
}