Move some specs from remote spec table into local repo (#116)

Added:
- Murat's PlusCal version of Lamport & Gray's analysis of Paxos vs. Two-Phase Commit
- Voucher Transaction System
- Atomic Commitment Protocol
- Byzantine Paxos

Signed-off-by: Andrew Helwer <[email protected]>

Author: ahelwer

.ciignore

@@ -5,3 +5,8 @@
 # Example:
 specifications/doesnotexist
 
+# Ignore submodules to ensure deterministic local execution
+specifications/BlockingQueue
+specifications/CCF
+specifications/azure-cosmos-tla
+

.github/scripts/format_markdown_table.py

@@ -18,42 +18,51 @@
 
 columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']
 
-def get_column(row, index):
+def get_column(row, col_name):
     '''
     Gets the cell of the given column in the given row.
     '''
-    return row.children[columns.index(index)].children[0]
+    return row.children[columns.index(col_name)].children[0]
 
-def remove_column(table, col_index):
+def remove_column(table, col_name):
     '''
     Removes the column of the given index from the table.
     '''
-    index = columns.index(col_index)
+    index = columns.index(col_name)
     table.header.children.pop(index)
     table.column_align.pop(index)
     for row in table.children:
         row.children.pop(index)
 
-def blank_column(table, col_index):
+def blank_column(table, col_name):
     '''
     Removes all data in the given column.
     '''
-    index = columns.index(col_index)
+    index = columns.index(col_name)
     for row in table.children:
         row.children[index].children = []
 
-def swap_columns(table, first_col_index, second_col_index):
+def duplicate_column(table, col_name):
+    '''
+    Duplicates the given column.
+    '''
+    index = columns.index(col_name)
+    table.header.children.insert(index, table.header.children[index])
+    table.column_align.insert(index, table.column_align[index])
+    for row in table.children:
+        row.children.insert(index, row.children[index])
+
+def swap_columns(table, first_col_name, second_col_name):
     '''
     Swaps two columns in a table.
     '''
-    first = columns.index(first_col_index)
-    second = columns.index(second_col_index)
+    first = columns.index(first_col_name)
+    second = columns.index(second_col_name)
     table.header.children[second], table.header.children[first] = table.header.children[first], table.header.children[second]
     table.column_align[second], table.column_align[first] = table.column_align[first], table.column_align[second]
     for row in table.children:
         row.children[second], row.children[first] = row.children[first], row.children[second]
 
-
 def format_table(table):
     '''
     All table transformations should go here.
@@ -65,8 +74,9 @@ def format_document(document):
     All document transformations should go here.
     '''
     # Gets table of local specs
-    table = next((child for child in document.children if isinstance(child, Table)))
-    format_table(table)
+    local_table, remote_table = [child for child in document.children if isinstance(child, Table)]
+    #format_table(local_table)
+    #format_table(remote_table)
 
 # Read, format, write
 # Need to both parse & render within same MarkdownRenderer context to preserve other formatting

.github/scripts/generate_manifest.py

@@ -78,7 +78,7 @@ def generate_new_manifest(examples_root, ignored_dirs, parser, queries):
                 'path': to_posix(spec_path),
                 'title': spec_name,
                 'description': '',
-                'source': '',
+                'sources': [],
                 'authors': [],
                 'tags': [],
                 'modules': [
@@ -116,10 +116,9 @@ def find_corresponding_spec(old_spec, new_manifest):
     return specs[0] if any(specs) else None
 
 def integrate_spec_info(old_spec, new_spec):
-    fields = ['title', 'description', 'source', 'tags']
+    fields = ['title', 'description', 'authors', 'sources', 'tags']
     for field in fields:
         new_spec[field] = old_spec[field]
-    new_spec['authors'] = old_spec['authors']
 
 def find_corresponding_module(old_module, new_spec):
     modules = [

.github/workflows/CI.yml

@@ -180,11 +180,13 @@ jobs:
             specifications/PaxosHowToWinATuringAward/Consensus.tla
             specifications/lamport_mutex/LamportMutex_proofs.tla
             specifications/ewd998/EWD998_proof.tla
+            specifications/byzpaxos/VoteProof.tla
             # Long-running; see https://github.com/tlaplus/tlapm/issues/85
             specifications/LoopInvariance/Quicksort.tla
             specifications/LoopInvariance/SumSequence.tla
             specifications/bcastByz/bcastByz.tla
             specifications/MisraReachability/ReachabilityProofs.tla
+            specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
           )
           python $SCRIPT_DIR/check_proofs.py  \
             --tlapm_path deps/tlapm-install   \