Skip to content

Commit

Permalink
YARN-913 Initial yarn registry just to get the git process booted
Browse files Browse the repository at this point in the history
  • Loading branch information
steveloughran committed Sep 1, 2014
1 parent e53813b commit 40f777b
Show file tree
Hide file tree
Showing 2 changed files with 62 additions and 1 deletion.
6 changes: 5 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -13,4 +13,8 @@ hs_err_pid*

# Tex artifacts
*.dvi
*.aux
*.aux
*.pdf
*.log
.project
*.toolbox
57 changes: 57 additions & 0 deletions tlaspecs/yarnregistry/yarnregistry.tla
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
---------------------------- MODULE yarnregistry ----------------------------


EXTENDS Sequences

(* a path element is all chars excluding "/" *)

CONSTANTS
PathChars, \* the set of valid characters in a path
Paths, \* the set of all possible valid paths
Data \* the set of all possible sequences of bytes



(* all paths in the system *)
VARIABLE registryPaths

PathCharInvariant == PathChars \subseteq STRING

PathInvariant == \A p \in registryPaths: \A pe \in p : pe \in PathChars

(*
isRoot[P] == p = []
*)
(* parent(p, q) == *)

=============================================================================

(*
An Entry is defined as a path, an ephemerality flag, and the actual data which it contains.

By including the path in an entry, we avoid having to define some function
mapping Path -> entry. Instead a registry can be defined as a set of RegistryEntries
matching the validity critera.

*)

RegistryEntry == [
path: Paths, \* The path to the entry
ephemeral: BOOLEAN, \* A flag to indicate when the entry is ephemeral
data: Data] \* the data in the entry


(***************************************************************************
For validity, all entries must match the following criteria

* there can be at most one entry with a given path in the set
* their path is either [] or a parent path which must also be found in the registry
* no entry may have a parent that is ephemeral

***************************************************************************)

=============================================================================
=============================================================================
\* Modification History
\* Last modified Mon Sep 01 18:50:01 BST 2014 by stevel
\* Created Sun Aug 31 14:54:47 BST 2014 by stevel

0 comments on commit 40f777b

Please sign in to comment.