diff --git a/.gitmodules b/.gitmodules index f8978d3025..21e5ea26e8 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1094,6 +1094,9 @@ [submodule "vendor/grammars/quakec-syntax"] path = vendor/grammars/quakec-syntax url = https://github.com/4LT/quakec-syntax.git +[submodule "vendor/grammars/quint-grammars"] + path = vendor/grammars/quint-grammars + url = https://github.com/informalsystems/quint-grammars.git [submodule "vendor/grammars/r.tmbundle"] path = vendor/grammars/r.tmbundle url = https://github.com/textmate/r.tmbundle diff --git a/grammars.yml b/grammars.yml index a7db2d7ed1..4b61493a39 100644 --- a/grammars.yml +++ b/grammars.yml @@ -1005,6 +1005,8 @@ vendor/grammars/quake: - source.quake vendor/grammars/quakec-syntax: - source.quakec +vendor/grammars/quint-grammars: +- source.quint vendor/grammars/r.tmbundle: - source.r - text.tex.latex.rd diff --git a/lib/linguist/languages.yml b/lib/linguist/languages.yml index a1e2ed2f67..04c0409e11 100644 --- a/lib/linguist/languages.yml +++ b/lib/linguist/languages.yml @@ -6267,6 +6267,14 @@ QuickBASIC: codemirror_mode: vb codemirror_mime_type: text/x-vb language_id: 593107205 +Quint: + type: programming + color: "#9d6ce5" + extensions: + - ".qnt" + tm_scope: source.quint + ace_mode: text + language_id: 562056483 R: type: programming color: "#198CE7" diff --git a/samples/Quint/LamportMutex.qnt b/samples/Quint/LamportMutex.qnt new file mode 100644 index 0000000000..22e3a7f07f --- /dev/null +++ b/samples/Quint/LamportMutex.qnt @@ -0,0 +1,183 @@ +module LamportMutex { + // This is a typed version of LamportMutex, which can be found at: + // https://github.com/tlaplus/Examples/blob/master/specifications/lamport_mutex/LamportMutex.tla + + /***************************************************************************/ + /* TLA+ specification of Lamport's distributed mutual-exclusion algorithm */ + /* that appeared as an example in */ + /* L. Lamport: Time, Clocks and the Ordering of Events in a Distributed */ + /* System. CACM 21(7):558-565, 1978. */ + /***************************************************************************/ + + // The parameter N represents the number of processes. + const N: int + // The parameter maxClock is used only for model checking in order to + // keep the state space finite. + const maxClock: int + + assume NType = N.in(Nat) + assume maxClockType = maxClock.in(Nat) + + val Proc = 1.to(N) + val Clock = Nat.exclude(Set(0)) + + /* For model checking, add ClockConstraint as a state constraint to ensure + a finite state space and override the definition of Clock by + 1 .. maxClock+1 so that TLC can evaluate the definition of Message. */ + + // local clock of each process + var clock: int -> int + // requests received from processes (clock transmitted with request) + var req: int -> (int -> int) + // acknowledgements received from processes + var ack: int -> Set[int] + // set of processes in critical section + var crit: Set[int] + // messages sent but not yet received + var network: int -> (int -> List[{ mtype: str, clock: int }]) + + // Messages used in the algorithm. + def ReqMessage(c) = { mtype: "req", clock: c } + val AckMessage = { mtype: "ack", clock: 0 } + val RelMessage = { mtype: "rel", clock: 0 } + + val Message = Set(AckMessage, RelMessage).union(Clock.map(c => ReqMessage(c))) + + action Init = all { + clock' = Proc.mapBy(p => 0), + req' = Proc.mapBy(p => Proc.mapBy(q => 0)), + ack' = Proc.mapBy(p => Set()), + network' = Proc.mapBy(p => Proc.mapBy(q => List())), + crit' = Set(), + } + + /* beats(p,q) is true if process p believes that its request has higher + priority than q's request. This is true if either p has not received a + request from q or p's request has a smaller clock value than q's. + If there is a tie, the numerical process ID decides. */ + def beats(p, q) = or { + req.get(p).get(q) == 0, + req.get(p).get(p) < req.get(p).get(q), + req.get(p).get(p) == req.get(p).get(q), + p < q, + } + + // Broadcast a message: send it to all processes except the sender. + def Broadcast(s, m) = Proc.mapBy(r => + if (r == s) + network.get(s).get(r) + else + network.get(s).get(r).append(m) + ) + + // Process p requests access to critical section. + action Request(p) = all { + req.get(p).get(p) == 0, + req' = req.setBy(p, r => r.setBy(p, c => clock.get(p))), + network' = network.setBy(p, n => Broadcast(p, ReqMessage(clock.get(p)))), + ack' = ack.set(p,Set(p)), + clock' = clock, + crit' = crit, + } + + // Process p receives a request from q and acknowledges it. + action ReceiveRequest(p,q) = all { + network.get(p).get(q) != List(), + val m = network.get(q).get(p).head() + val c = m.clock + all { + m.mtype == "req", + req' = req.setBy(p, a => a.setBy(q, b => c)), + clock' = clock.setBy(p, a => if (c > a) c + 1 else a + 1), + network' = network.setBy(q, a => a.setBy(p, b => b.tail())) + .setBy(p, a => a.setBy(q, b => b.append(AckMessage))), + }, + ack' = ack, + crit' = crit, + } + + // Process p receives an acknowledgement from q. + action ReceiveAck(p, q) = all { + network.get(p).get(q) != List(), + val m = network.get(p).get(q).head() all { + m.mtype == "ack", + network' = network.setBy(p, a => a.setBy(q, b => b.tail())), + ack' = ack.setBy(p, a => a.union(Set(q))), + }, + clock' = clock, + req' = req, + crit' = crit, + } + + // Process p enters the critical section. + action Enter(p) = all { + ack.get(p) == Proc, + Proc.forall(q => beats(p, q)), + crit' = crit.union(Set(p)), + clock' = clock, + req' = req, + ack' = ack, + network' = network, + } + + // Process p exits the critical section and notifies other processes. + action Exit(p) = all { + p.in(crit), + crit' = crit.exclude(Set(p)), + network' = network.set(p, Broadcast(p, RelMessage)), + req' = req.setBy(p, r => r.set(p, 0)), + ack' = ack.set(p, Set()), + clock' = clock, + } + + // Process p receives a release notification from q. + action ReceiveRelease(p,q) = all { + network.get(p).get(q) != List(), + val m = network.get(p).get(q).head() all { + m.mtype == "rel", + req' = req.setBy(p, r => r.set(q, 0)), + network' = network.setBy(p, a => a.setBy(q, b => b.tail())), + }, + clock' = clock, + ack' = ack, + crit' = crit, + } + + // Next-state relation. + action Next = { + nondet p = oneOf(Proc) + any { + Request(p), + Enter(p), + Exit(p), + nondet q = oneOf(Proc) + any { + ReceiveRequest(p,q), + ReceiveAck(p,q), + ReceiveRelease(p,q), + } + } + } + + /* A state constraint that is useful for validating the specification + using finite-state model checking. */ + val ClockConstraint = Proc.forall(p => (clock.get(p) <= maxClock)) + + /* No channel ever contains more than three messages. In fact, no channel + ever contains more than one message of the same type, as proved below.*/ + val BoundedNetwork = Proc.forall(p => + Proc.forall(q => + network.get(p).get(q).length() <= 3 + ) + ) + + // The main safety property of mutual exclusion. + val Mutex = crit.forall(p => crit.forall(q => p == q)) +} + +module LamportMutex_3_10 { + import LamportMutex( + N = 3, + maxClock = 10 + ).* +} diff --git a/samples/Quint/Paxos.qnt b/samples/Quint/Paxos.qnt new file mode 100644 index 0000000000..b05d5689d6 --- /dev/null +++ b/samples/Quint/Paxos.qnt @@ -0,0 +1,300 @@ + +module Paxos { + /*************************************************************************** + * This is a specification of the Paxos algorithm without explicit leaders * + * or learners. It refines the spec in Voting * + ***************************************************************************/ + /*************************************************************************** + * The constant parameters and the set Ballots are the same as in Voting. * + ***************************************************************************/ + + const Value: Set[int] + + const Acceptor: Set[str] + + const Quorum: Set[Set[str]] + + assume _ = and { + Quorum.forall(Q => Q.subseteq(Acceptor)), + tuples(Quorum, Quorum).forall( ((Q1, Q2)) => (Q1.intersect(Q2)) != Set()) + } + + val Ballot = Nat + + val None = -1 + /************************************************************************* + * An unspecified value that is not a ballot number. * + *************************************************************************/ + + //----------------------------------------------------------------------------- + + var maxBal: str -> int + var maxVBal: str -> int // <> is the vote with the largest + var maxVal: str -> int // ballot number cast by a; it equals <<-1, None>> if + // a has not cast any vote. + + // Particular message types we need to refer to later: + type Msg1bT = { acceptor: str, bal: int, mbal: int, mval: int } + type Msg2aT = { bal: int, value: int } + + // A union type for records representing different types of messages. + type MSG = + | Msg1a({ bal: int }) + | Msg1b(Msg1bT) + | Msg2a(Msg2aT) + | Msg2b({ acc: str, bal: int, value: int }) + + var msgs: Set[MSG] // The set of all messages that have been sent. + + // Access the balance of a message, irrespictive of the message variant + def balance(m: MSG): int = match m { + | Msg1a(mm) => mm.bal + | Msg1b(mm) => mm.bal + | Msg2a(mm) => mm.bal + | Msg2b(mm) => mm.bal + } + + // Filter a set of messager into just 1b messages + def filterMsg1b(ms: Set[MSG]): Set[Msg1bT] = + ms.fold(Set(), (acc, m) => match m { + | Msg1b(m1b) => acc.union(Set(m1b)) + | _ => acc + }) + + // Filter a set of messager into just 2a messages + def filterMsg2a(ms: Set[MSG]): Set[Msg2aT] = + ms.fold(Set(), (acc, m) => match m { + | Msg2a(m2a) => acc.union(Set(m2a)) + | _ => acc + }) + + /***************************************************************************) + (* NOTE: *) + (* The algorithm is easier to understand in terms of the set msgs of all *) + (* messages that have ever been sent. A more accurate model would use *) + (* one or more variables to represent the messages actually in transit, *) + (* and it would include actions representing message loss and duplication *) + (* as well as message receipt. *) + (* *) + (* In the current spec, there is no need to model message loss because we *) + (* are mainly concerned with the algorithm's safety property. The safety *) + (* part of the spec says only what messages may be received and does not *) + (* assert that any message actually is received. Thus, there is no *) + (* difference between a lost message and one that is never received. The *) + (* liveness property of the spec that we check makes it clear what *) + (* messages must be received (and hence either not lost or successfully *) + (* retransmitted if lost) to guarantee progress. *) + (***************************************************************************/ + + val vars = (maxBal, maxVBal, maxVal, msgs) + /************************************************************************* + * It is convenient to define some identifier to be the tuple of all * + * variables. I like to use the identifier `vars'. * + *************************************************************************/ + + /***************************************************************************) + (* The type invariant and initial predicate. *) + (***************************************************************************/ + val TypeOK = and { + maxBal.in(Acceptor.setOfMaps(Ballot.union(Set(-1)))), + maxVBal.in(Acceptor.setOfMaps(Ballot.union(Set(-1)))), + maxVal.in(Acceptor.setOfMaps(Value.union(Set(None)))), + } + + action Init = all { + maxBal' = Acceptor.mapBy(_ => -1), + maxVBal' = Acceptor.mapBy(_ => -1), + maxVal' = Acceptor.mapBy(_ => None), + msgs' = Set(), + } + + /***************************************************************************) + (* The actions. We begin with the subaction (an action that will be used *) + (* to define the actions that make up the next-state action. *) + (***************************************************************************/ + action Send(m: MSG): bool = { + msgs' = msgs.union(Set(m)) + } + + /***************************************************************************) + (* In an implementation, there will be a leader process that orchestrates *) + (* a ballot. The ballot b leader performs actions Phase1a(b) and *) + (* Phase2a(b). The Phase1a(b) action sends a phase 1a message (a message *) + (* m with m.type = "1a") that begins ballot b. *) + (***************************************************************************/ + action Phase1a(b) = all { + Send(Msg1a({ bal: b })), + maxVBal' = maxVBal, + maxVal' = maxVal, + } + + /***************************************************************************) + (* Upon receipt of a ballot b phase 1a message, acceptor a can perform a *) + (* Phase1b(a) action only if b > maxBal[a]. The action sets maxBal[a] to *) + (* b and sends a phase 1b message to the leader containing the values of *) + (* maxVBal[a] and maxVal[a]. *) + (***************************************************************************/ + action Phase1b(a) = { + nondet m = msgs.filter(m2 => match m2 { Msg1a(_) => true | _ => false }).oneOf() + all { + m.balance() > maxBal.get(a), + Send(Msg1b({ acceptor: a, bal: m.balance(), mbal: maxVBal.get(a), mval: maxVal.get(a) })), + maxBal' = maxBal.set(a, m.balance()), + maxVBal' = maxVBal, + maxVal' = maxVal, + } + } + + /***************************************************************************) + (* The Phase2a(b, v) action can be performed by the ballot b leader if two *) + (* conditions are satisfied: (i) it has not already performed a phase 2a *) + (* action for ballot b and (ii) it has received ballot b phase 1b messages *) + (* from some quorum Q from which it can deduce that the value v is safe at *) + (* ballot b. These enabling conditions are the first two conjuncts in the *) + (* definition of Phase2a(b, v). This second conjunct, expressing *) + (* condition (ii), is the heart of the algorithm. To understand it, *) + (* observe that the existence of a phase 1b message m in msgs implies that *) + (* m.mbal is the highest ballot number less than m.bal in which acceptor *) + (* m.acc has or ever will cast a vote, and that m.mval is the value it *) + (* voted for in that ballot if m.mbal # -1. It is not hard to deduce from *) + (* this that the second conjunct implies that there exists a quorum Q such *) + (* that ShowsSafeAt(Q, b, v) (where ShowsSafeAt is defined in module *) + (* Voting). *) + (* *) + (* The action sends a phase 2a message that tells any acceptor a that it *) + (* can vote for v in ballot b, unless it has already set maxBal[a] *) + (* greater than b (thereby promising not to vote in ballot b). *) + (***************************************************************************/ + action Phase2a(b, v) = all { + not(msgs.exists(m => match m { Msg2a(m2a) => m2a.bal == b | _ => false })), + Quorum.exists(Q => + val Q1b = msgs.filterMsg1b() + .filter(m => (m.acceptor.in(Q)) and (m.bal == b)) + val Q1bv = Q1b.filter(m => m.mbal >= 0) + and { + Q.forall(a => Q1b.exists(m => m.acceptor == a)), + or { + Q1bv == Set(), + Q1bv.exists(m => or { + m.mval == v, + Q1bv.forall(mm => m.mbal >= mm.mbal) + }) + } + } + ), + Send(Msg2a({ bal: b, value: v })), + maxVBal' = maxVBal, + maxVal' = maxVal, + } + + /***************************************************************************) + (* The Phase2b(a) action is performed by acceptor a upon receipt of a *) + (* phase 2a message. Acceptor a can perform this action only if the *) + (* message is for a ballot number greater than or equal to maxBal[a]. In *) + (* that case, the acceptor votes as directed by the phase 2a message, *) + (* setting maxVBal[a] and maxVal[a] to record that vote and sending a *) + (* phase 2b message announcing its vote. It also sets maxBal[a] to the *) + (* message's. ballot number *) + (***************************************************************************/ + action Phase2b(a) = { + nondet m = msgs.filterMsg2a().oneOf() + all { + m.bal >= maxBal.get(a), + Send(Msg2b({ acc: a, bal: m.bal, value: m.value })), + maxBal' = maxBal.set(a, m.bal), + maxVBal' = maxVBal.set(a, m.bal), + maxVal' = maxVal.set(a, m.value), + } + } + + /***************************************************************************) + (* In an implementation, there will be learner processes that learn from *) + (* the phase 2b messages if a value has been chosen. The learners are *) + (* omitted from this abstract specification of the algorithm. *) + (***************************************************************************/ + + /***************************************************************************) + (* Below are defined the next-state action and the complete spec. *) + (***************************************************************************/ + action Next = any { + all { + nondet b = oneOf(Ballot) + any { + Phase1a(b), + nondet v = oneOf(Value) + Phase2a(b, v) + }, + maxBal' = maxBal, + }, + nondet a = oneOf(Acceptor) + any { + Phase1b(a), + Phase2b(a), + } + } + + //---------------------------------------------------------------------------- + /***************************************************************************) + (* We now define the refinement mapping under which this algorithm *) + (* implements the specification in module Voting. *) + (***************************************************************************/ + + /***************************************************************************) + (* As we observed, votes are registered by sending phase 2b messages. So *) + (* the array `votes' describing the votes cast by the acceptors is defined *) + (* as follows. *) + (***************************************************************************/ + val votes = + Acceptor.mapBy(a => + msgs.fold(Set(), (acc, mm) => + match mm { + | Msg2b(m) => if (m.acc == a) acc.union(Set((m.bal, m.value))) else acc + | _ => acc })) + + /***************************************************************************) + (* We now instantiate module Voting, substituting the constants Value, *) + (* Acceptor, and Quorum declared in this module for the corresponding *) + (* constants of that module Voting, and substituting the variable maxBal *) + (* and the defined state function `votes' for the correspondingly-named *) + (* variables of module Voting. *) + (***************************************************************************/ + + + import Voting(Value = Value, Acceptor = Acceptor, Quorum = Quorum) as V from "./Voting" + + // Like theorems? Then you should definitely go straight for TLA+ + // THEOREM Spec => V!Spec + //----------------------------------------------------------------------------- + /***************************************************************************) + (* Here is a first attempt at an inductive invariant used to prove this *) + (* theorem. *) + (***************************************************************************/ + val Inv = and { + TypeOK, + Acceptor.forall(a => + if (maxVBal.get(a) == -1) + maxVal.get(a) == None + else (maxVBal.get(a), maxVal.get(a)).in(votes.get(a)) + ), + msgs.filterMsg1b() + .forall(m => + (maxBal.get(m.acceptor) >= m.bal + and ((m.mbal >= 0) implies (m.mbal, m.mval).in(votes.get(m.acceptor))))), + val M2as = msgs.filterMsg2a() + M2as.forall(m => and { + Quorum.exists(Q => V::ShowsSafeAt(Q, m.bal, m.value)), + M2as.forall(mm => + (mm.bal == m.bal) implies (mm.value == m.value) + ), + }), + V::Inv, + } +} + +module Paxos_val2_accept3_quorum2 { + import Paxos( + Value = Set(0, 1), + Acceptor = Set("a1", "a2", "a3"), + Quorum = Set(Set("a1", "a2")) + ).* +} diff --git a/samples/Quint/clockSync6.qnt b/samples/Quint/clockSync6.qnt new file mode 100644 index 0000000000..bc9425776b --- /dev/null +++ b/samples/Quint/clockSync6.qnt @@ -0,0 +1,192 @@ +/** + * Clock Synchronization Algorithm - Version 6 (from TLA+ ClockSync6) + * + * This specification is a Quint translation of the TLA+ model ClockSync6.tla + * from the tla-apalache-workshop [1]. + * + * Check with: + * quint verify clockSync6.qnt --invariant skew_inv --main clock_sync4 + * + * [1]: https://github.com/informalsystems/tla-apalache-workshop/blob/main/examples/clock-sync/ClockSync6.tla + */ +module clock_sync { + import basicSpells.* from "../../../spells/basicSpells" + + /* CONSTANTS */ + + /// The set of processes + const processes: Set[str] + /// Minimum message delay + const t_min: int + /// Maximum message delay + const t_max: int + + assume _ = (t_min >= 0 and t_max > t_min) + + /* TYPES */ + + type ControlState = Init | Sent | Sync + + type Message = { src: str, timestamp: int } + + type State = { + process_id: str, + hardware_clock: int, + clock_adjustment: int, + diffs: str -> int, + received_messages: Set[Message], + control_state: ControlState, + } + + /* State Variables */ + + /// The reference clock, inaccessible to the processes + var time: int + /// Messages sent by the processes + var messages: Set[Message] + /// The local state of each process + var states: str -> State + + /* DEFINITIONS */ + + /// Sum up the clock differences as observed by a process p + pure def diff_sum(s: State): int = { + s.diffs.values().fold(0, (total, d) => total + d) + } + + /// If the process has received a message from all processes (but p), + /// then adjust the clock. + pure def adjust_clock(s: State): State = { + if (s.received_messages.map(m => m.src) == processes.setRemove(s.process_id)) + // Adjust the clock + { + ...s, + clock_adjustment: diff_sum(s) / processes.size(), + control_state: Sync, + } + else + s + } + + /* ACTIONS */ + + /// Send the value of the hardware clock + action send_msg(s: State): bool = all { + s.control_state == Init, + messages' = messages.setAdd({ src: s.process_id, timestamp: s.hardware_clock }), + states' = states.set(s.process_id, { ...s, control_state: Sent }), + time' = time, + } + + // Receive a message sent by another process. + // Adjust the clock if the message has been received from all other processes. + action receive_msg(s: State): bool = all { + s.control_state == Sent, + + val potential_messages = messages.filter(m => + // Not already received + not(m.in(s.received_messages)) and + // Not from itself + m.src != s.process_id and + // The message cannot be received earlier than after t_min + // (enforced by the system, the process can't control this) + states.get(m.src).hardware_clock >= m.timestamp + t_min + ) + + all { + potential_messages != Set(), + // This choice implies a precondition that the filtered set is non-empty + nondet m = oneOf(potential_messages) + + // Accumulate the difference and adjust the clock if possible + val delta = m.timestamp - s.hardware_clock + (t_min + t_max) / 2 + val new_state = { + ...s, + received_messages: s.received_messages.union(Set(m)), + diffs: s.diffs.set(m.src, delta), + } + states' = states.set(s.process_id, adjust_clock(new_state)), + time' = time, + messages' = messages, + } + } + + // Let the time flow + action advance_clocks(delta_param: int): bool = all { + delta_param > 0, + // Clocks can be advanced only if there is no pending message + messages.forall(m => + states.get(m.src).hardware_clock + delta_param > t_max + implies states.values().forall(s => + m.in(s.received_messages) + ) + ), + time' = time + delta_param, + states' = states.transformValues(s => { + ...s, + hardware_clock: s.hardware_clock + delta_param + }), + messages' = messages, + } + + action init = all { + time' = 0, + messages' = Set(), + states' = processes.mapBy(p => { + process_id: p, + hardware_clock: 0, + clock_adjustment: 0, + diffs: processes.mapBy(_ => 0), + control_state: Init, + received_messages: Set(), + }) + } + + action step = any { + // Option 1: Advance clocks + nondet delta = oneOf(Int) + advance_clocks(delta), + + // Option 2: A process performs an action + nondet s = oneOf(states.values()) + any { + s.send_msg(), + s.receive_msg(), + } + } + + /* Properties */ + + /// The adjusted clock of process i_proc + def adjusted_clock(i_proc: str): int = { + val s = states.get(i_proc) + s.hardware_clock + s.clock_adjustment + } + + // Theorem 6.15 from AW04: + // Algorithm achieves u * (1 - 1/n)-synchronization for n processors. + val skew_inv: bool = { + val all_sync = states.values().forall(s => s.control_state == Sync) + + val bounded_skew = { + val N = processes.size() + // extend the bound by N to account for rounding errors + val bound = (t_max - t_min) * (N - 1) + N * N + processes.forall(p => + processes.forall(q => { + val df = p.adjusted_clock() - q.adjusted_clock() + -bound <= df * N and df * N <= bound + }) + ) + } + all_sync implies bounded_skew + } +} + +module clock_sync4 { + import clock_sync( + processes = Set("p1", "p2", "p3", "p4"), + t_min = 17, + t_max = 91 + ).* +} diff --git a/vendor/README.md b/vendor/README.md index cfa3e60857..16dc5ed272 100644 --- a/vendor/README.md +++ b/vendor/README.md @@ -513,6 +513,7 @@ This is a list of grammars that Linguist selects to provide syntax highlighting - **Quake:** [newgrammars/quake](https://github.com/newgrammars/quake) - **QuakeC:** [4LT/quakec-syntax](https://github.com/4LT/quakec-syntax) - **QuickBASIC:** [QB64Official/vscode](https://github.com/QB64Official/vscode) +- **Quint:** [informalsystems/quint-grammars](https://github.com/informalsystems/quint-grammars) - **R:** [textmate/r.tmbundle](https://github.com/textmate/r.tmbundle) - **RAML:** [atom/language-yaml](https://github.com/atom/language-yaml) - **RAScript:** [joshraphael/rascript-syntax](https://github.com/joshraphael/rascript-syntax) diff --git a/vendor/grammars/quint-grammars b/vendor/grammars/quint-grammars new file mode 160000 index 0000000000..58f1a697fa --- /dev/null +++ b/vendor/grammars/quint-grammars @@ -0,0 +1 @@ +Subproject commit 58f1a697fa8bcdfe3239a77db48b0a6b9888fc29 diff --git a/vendor/licenses/git_submodule/quint-grammars.dep.yml b/vendor/licenses/git_submodule/quint-grammars.dep.yml new file mode 100644 index 0000000000..1df9173d13 --- /dev/null +++ b/vendor/licenses/git_submodule/quint-grammars.dep.yml @@ -0,0 +1,33 @@ +--- +name: quint-grammars +version: 58f1a697fa8bcdfe3239a77db48b0a6b9888fc29 +type: git_submodule +homepage: https://github.com/informalsystems/quint-grammars.git +license: mit +licenses: +- sources: LICENSE + text: | + MIT License + + Copyright (c) 2026 Informal Systems + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. +- sources: README.md + text: MIT — see [LICENSE](./LICENSE). +notices: []