Default package

Get desktop application:
View/edit binary Protocol Buffers messages

Used in: File, Role

• optional SourceInfo source_info = 1

• string name = 2

• Flow flow = 3

• optional Fairness fairness = 4

• optional Block block = 5

Used in: Statement

• optional SourceInfo source_info = 1

• Flow flow = 2

• repeated string loop_vars = 3

• string py_expr = 4

• optional Block block = 5

• string condition = 6

• optional Expr iter_expr = 7

• optional Expr condition_expr = 8

• optional Fairness fairness = 9

The actual arguments to a function/method call. For example, in `foo(4, 5)`, `4` and `5` are arguments.

Used in: CallStmt, Decorator

• optional SourceInfo source_info = 1

• string name = 2

• string py_expr = 3

• optional Expr expr = 4

Used in: Action, AnyStmt, Branch, ForStmt, Function, Invariant, Statement, WhileStmt

• optional SourceInfo source_info = 1

• Flow flow = 2

• repeated Statement stmts = 3

Used in: IfStmt

• optional SourceInfo source_info = 1

• string condition = 2

• optional Block block = 3

• optional Expr condition_expr = 4

Used in: Statement

• optional SourceInfo source_info = 1

Used in: Statement

• optional SourceInfo source_info = 1

• repeated string vars = 2

• string name = 3

• repeated Argument args = 4

• string receiver = 5

Used in: Row

• bool has_link = 1

• string name = 2

• repeated string labels = 3

Used in: File

• optional SourceInfo source_info = 1

• string name = 2

Used in: Statement

• optional SourceInfo source_info = 1

Counter defines the metric to be collected. This can be used to collect the number of times a branch is taken. Or other cost metrics like resource usage, or price. This is equivalent to reward in PRISM. For now, supports only simple numberic values. Eventually, this should support distributions like normal, exponential, etc.

Used in: TransitionConfig

• double numeric = 1

  The value to be added to the counter.

Used in: Role

• optional SourceInfo source_info = 1

• string name = 2

• repeated Argument args = 3

Used in: AnyStmt, Argument, Branch, ForStmt, Parameter, RequireStmt, ReturnStmt, WhileStmt

• optional SourceInfo source_info = 1

• string py_expr = 2

Used in: Action, AnyStmt

• optional SourceInfo source_info = 1

• FairnessLevel level = 2

Used in: Fairness

• FAIRNESS_LEVEL_UNKNOWN = 0

• FAIRNESS_LEVEL_UNFAIR = 1

• FAIRNESS_LEVEL_WEAK = 2

• FAIRNESS_LEVEL_STRONG = 3

• optional SourceInfo source_info = 1

• repeated Import imports = 2

• repeated Constant constants = 3

• optional StateVars states = 4

• repeated Invariant invariants = 6

  StateVars variables = 5; Action init = 5;

• repeated Action actions = 7

• repeated Function functions = 8

• repeated Statement stmts = 9

• repeated Role roles = 10

• repeated string py_code = 11

• optional FrontMatter front_matter = 12

Used in: Action, AnyStmt, Block, ForStmt, Function, IfStmt, WhileStmt

• FLOW_UNKNOWN = 0

• FLOW_SERIAL = 1

• FLOW_PARALLEL = 2

• FLOW_ATOMIC = 3

• FLOW_ONEOF = 4

Used in: Statement

• optional SourceInfo source_info = 1

• Flow flow = 2

• repeated string loop_vars = 3

• string py_expr = 4

• optional Block block = 5

• optional Expr iter_expr = 6

Used in: File

• optional SourceInfo source_info = 1

• string yaml = 2

Used in: File, Role

• optional SourceInfo source_info = 1

• string name = 2

• Flow flow = 3

• repeated Parameter params = 4

• optional Block block = 5

Used in: Statement

• optional SourceInfo source_info = 1

• Flow flow = 2

• repeated Branch branches = 3

Used in: File

• optional SourceInfo source_info = 1

• string path = 2

• string alias = 3

Used in: File, Role

• optional SourceInfo source_info = 1

• bool always = 2

• bool eventually = 3

• string pyExpr = 4

• optional Invariant nested = 5

• string name = 6

• repeated string temporal_operators = 7

• optional Block block = 8

• string py_code = 9

• repeated Parameter params = 10

Used in: Links

• int64 src = 1

• int64 dest = 2

• string name = 3

• repeated string labels = 4

• double weight = 5

• repeated Message messages = 6

• int64 req_id = 7

• map<int64, int64> new_to_old_threads = 8

• string type = 9

• int64 total_nodes = 1

• repeated Link links = 2

• repeated Row rows = 1

Used in: Link

• string sender = 1

• repeated string receivers = 2

• string name = 3

• repeated NameValue values = 4

• bool is_return = 5

• bool lossy = 6

Used in: Message

• string name = 1

• string value = 2

• repeated string json = 1

Used in: StateSpaceOptions

• int64 max_actions = 1

• int64 max_concurrent_actions = 2

• optional bool crash_on_yield = 3

  If true (default), model checker would evaluate the possibility of a crash at yield points.

Variables in the function/method declaration. For example, in `def foo(x, y)`, `x` and `y` are parameters.

Used in: Function, Invariant

• optional SourceInfo source_info = 1

• string name = 2

• string default_py_expr = 3

• optional Expr default_expr = 4

• map<string, TransitionConfig> configs = 1

Used in: SourceInfo

• int32 line = 2

  int32 offset = 1;

• int32 column = 3

Used in: Statement

• optional SourceInfo source_info = 1

• string code = 2

Used in: Statement

• optional SourceInfo source_info = 1

• string condition = 2

• optional Expr condition_expr = 3

Used in: Statement

• optional SourceInfo source_info = 1

• string py_expr = 2

• optional Expr expr = 3

Used in: File

• optional SourceInfo source_info = 1

• string name = 2

• repeated string modifiers = 3

• optional StateVars states = 4

• repeated Invariant invariants = 6

• repeated Action actions = 7

• repeated Function functions = 8

• repeated Statement stmts = 9

• repeated Decorator decorators = 10

Used in: Matrix

• repeated Cell cells = 1

Used in: Action, AnyStmt, Argument, Block, Branch, BreakStmt, CallStmt, Constant, ContinueStmt, Decorator, Expr, Fairness, File, ForStmt, FrontMatter, Function, IfStmt, Import, Invariant, Parameter, PyStmt, RequireStmt, ReturnStmt, Role, StateVars, Statement, WhileStmt

• string file_name = 1

• optional Position start = 2

• optional Position end = 3

• optional Options options = 1

• map<string, Options> action_options = 2

  Set options like max_actions for individual action instead.

• bool continue_on_invariant_failures = 3

  If true, continue exploring the state space of other paths that did not fail.

• bool continue_path_on_invariant_failures = 4

  If true, continue the failed path as well, ignoring the invariant failure. This is almost equivalent to not having the invariant at all, but it can be useful for debugging

• string liveness = 5

  Default is 'strict' implies liveness check is done TLA+, the other options are 'probabilistic' The probabilisitic model checker is not integrated into the playground but has to be run separately in commandline.

• optional bool deadlock_detection = 6

  Enable (default/true) or disable deadlock detection Note: explicitly setting it optional, makes this tristate

Used in: File, Role

• optional SourceInfo source_info = 1

• string code = 2

Used in: Block, File, Role

• optional SourceInfo source_info = 1

• string label = 2

• optional PyStmt py_stmt = 3

• optional Block block = 4

• optional IfStmt if_stmt = 5

• optional ForStmt for_stmt = 6

• optional AnyStmt any_stmt = 7

• optional WhileStmt while_stmt = 8

• optional BreakStmt break_stmt = 9

• optional ContinueStmt continue_stmt = 10

• optional ReturnStmt return_stmt = 11

• optional CallStmt call_stmt = 12

• optional RequireStmt require_stmt = 13

Used in: PerformanceModel

• double probability = 1

  The probability for the branch to be taken.

• map<string, Counter> counters = 2

Used in: Statement

• optional SourceInfo source_info = 1

• Flow flow = 2

• string py_expr = 3

• optional Block block = 4

• optional Expr iter_expr = 5