Skip to content

Commit

Permalink
Fix bluespec definitions
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Oct 2, 2023
1 parent ca50ee2 commit a80ce70
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 5 deletions.
2 changes: 1 addition & 1 deletion tests/difference/core/quint_model/ccv.qnt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// -- mode: Bluespec; --
// -*- mode: Bluespec; -*-
module CCVTypes {
import Time.* from "./libraries/Time"

Expand Down
2 changes: 1 addition & 1 deletion tests/difference/core/quint_model/ccv_statemachine.qnt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// -- mode: Bluespec; --
// -*- mode: Bluespec; -*-
module CCVDefaultStateMachine {
// A basic state machine that utilizes the CCV protocol.
import CCVTypes.* from "./ccv"
Expand Down
3 changes: 1 addition & 2 deletions tests/difference/core/quint_model/libraries/Time.qnt
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
// -- mode: Bluespec; --

// -*- mode: Bluespec; -*-
// A simple module for time that makes timings more readable,
// e.g. 5 * Minute.
// The base unit are seconds, i.e. to get the number of seconds in a time value, just treat it as an int.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// -- mode: Bluespec; --
// -*- mode: Bluespec; -*-

// This module is just a library with utility functions (sometimes called spells in Quint).
module extraSpells {
Expand Down

0 comments on commit a80ce70

Please sign in to comment.