Constant mikino_api::TRANS_DEMO

pub const TRANS_DEMO: &str = "//! A simple demo hsmt transition system.\n//!\n//! Systems are declared in four ordered parts:\n//!\n//! - state variables of the system, `state`;\n//! - initial predicate, `init`;\n//! - transition predicate, `trans`;\n//! - candidates to try to prove on the system, `candidates`.\n//!\n//! # Init\n//!\n//! The initial predicate is a constraint over the variables of the system. Any assignment of the\n//! variables that makes this initial predicate true is a legal initial state.\n//!\n//! Say your system is just a counter with a single variable `cnt: int`. If you want to start with\n//! `cnt` equal to `0`, then your initial predicate would be `cnt = 0`. If you want to start with\n//! any positive value, then it would be `cnt >= 0` or `cnt \u{2265} 0`. If you\'re fine with starting with\n//! any value at all, then your initial predicate can just be `true` (or `\u{22a4}`) to leave `cnt`\n//! unconstrained.\n//!\n//! # Trans\n//!\n//! The transition predicate describes whether a state can be the successor of another state, or the\n//! \"next\" state. That is, the transition predicate is a constraint that mentions variables of the\n//! \"current\" state and variables of the \"next\" state. If `v` is a variable of your system, then the\n//! \"current\" value of `v` is just written `v`. The \"next\" value is written `\'v`.\n//!\n//! Going back to the simple counter system example above, you can express that the \"next\" value of\n//! `cnt` is the current value plus one with `\'cnt = cnt + 1`\n//!\n//! # Candidates\n//!\n//! A candidate is a *name* and a definition, *i.e.* a predicate over the variables of the system.\n//! The name is given as a double-quoted string, for instance `\"my candidate\"`. The predicate is a\n//! constraint over the variables. It cannot be a relation, *i.e.* mention *next-state variables*\n//! like `\'v`.\n//!\n//! In the counter system from above, maybe we want to prove that `cnt` is always positive. We can\n//! do so by having a PO called, for instance, `\"cnt is positive\"` defined as `cnt >= 0` or `cnt \u{2265}\n//! 0`.\n//!\n//! # This Example\n//!\n//! This system is a stopwatch. It has a (time) counter `cnt`, which would be the time a real\n//! stopwatch would actually display. It has two boolean variables `stop` and `reset` which would be\n//! buttons on an actual stopwatch. Variable `reset` forces `cnt` to be `0` whenever it is true,\n//! while `stop` freezes the value of `cnt` as long as it remains true. Note that `reset` has\n//! priority over `stop`: if both are true then `cnt` will be forced to `0`.\n//!\n//! # Notes on Operators and Literals\n//!\n//! Several operators can take more than one UTF8 or ASCII form.\n//!\n//! - conjunction: `and`, `&&`, `\u{2227}`, `\u{22c0}`\n//! - disjunction: `or` `||`, `\u{2228}`, `\u{22c1}`\n//! - implication: `=>`, `\u{21d2}`, `\u{2192}`, `\u{2283}`\n//! - negation: `not`, `!`, `\u{ac}`\n//! - arithmetic comparison: `>`, `>=`, `\u{2265}`, `<=`, `\u{2264}`, `<`\n//!\n//! If-then-else-s are written Rust-style: `if <cnd> { <thn> } else { <els> }` where `<cnd>` is a\n//! boolean expression, and `<thn>` and `<els>` are expressions of the same type. Rust\'s `else if`-s\n//! are also supported: `if c_1 { t_1 } else if c_2 { t_2 } .... else { e }`.\n\n/// Variables.\nsvars {\n    /// Stop button (input).\n    stop\n    /// Reset button (input).\n    reset: bool,\n    /// Time counter (output).\n    cnt: int,\n}\n\n/// Initial predicate.\n/// \n/// Comma-separated list of stateless expressions, with optional trailing comma.\ninit {\n    // `cnt` can be anything as long as it is positive.\n    cnt \u{2265} 0,\n    // if `reset`, then `cnt` has to be `0`.\n    (reset \u{21d2} cnt = 0),\n}\n\n/// Transition predicate.\n/// \n/// Comma-separated list of stateful expressions, with optional trailing comma.\n/// \n/// - `reset` has priority over `stop`;\n/// - the `ite` stands for \"if-then-else\" and takes a condition, a `then` expression and an `else`\n///   expression. These last two expressions must have the same type. In the two `ite`s below, that\n///   type is always `bool`.\ntrans {\n    \'cnt = if \'reset {\n        0\n    } else if \'stop {\n        cnt\n    } else {\n        cnt + 1\n    },\n}\n\n/// Proof obligations.\ncandidates {\n    \"cnt is positive\": cnt \u{2265} 0,\n    \"cnt is not -7\": \u{ac}(cnt = -7),\n    \"if reset then cnt is 0\": reset \u{21d2} cnt = 0,\n}";

String representation of a simple demo system.