Skip to content

Instantly share code, notes, and snippets.

@bennn
Created March 24, 2022 15:11
Show Gist options
  • Save bennn/c28d348aba3d0bbcfbad00fca8527ead to your computer and use it in GitHub Desktop.
Save bennn/c28d348aba3d0bbcfbad00fca8527ead to your computer and use it in GitHub Desktop.
cs1710-roboTrain
#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
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment