Fix unordered bulletted list

Use asciidoc to make doc match LaTeX unordered bulletted list.

1 files changed, 41 insertions, 22 deletions

diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc
index 2d62438..513c6d3 100644
--- a/src/mm-formal.adoc
+++ b/src/mm-formal.adoc
@@ -525,7 +525,7 @@ a construction of the post-transition model state for each.
 
 Transitions for all instructions:
 
-latexmath:[$\bullet$] <<fetch, Fetch instruction>>: This transition represents a fetch and decode of a new instruction instance, as a program order successor of a previously fetched
+* <<fetch, Fetch instruction>>: This transition represents a fetch and decode of a new instruction instance, as a program order successor of a previously fetched
 instruction instance (or the initial fetch address).
 
 The model assumes the instruction memory is fixed; it does not describe
@@ -534,16 +534,17 @@ not generate memory load operations, and the shared memory is not
 involved in the transition. Instead, the model depends on an external
 oracle that provides an opcode when given a memory location.
 
-latexmath:[$\circ$] <<reg_write, Register write>>: This is a write of a register value.
+[circle]
+* <<reg_write, Register write>>: This is a write of a register value.
 
-latexmath:[$\circ$] <<reg_read, Register read>>: This is a read of a register value from the most recent
+* <<reg_read, Register read>>: This is a read of a register value from the most recent
 program-order-predecessor instruction instance that writes to that
 register.
 
-latexmath:[$\circ$] <<sail_interp, Pseudocode internal step>>: This covers pseudocode internal computation: arithmetic, function
+* <<sail_interp, Pseudocode internal step>>: This covers pseudocode internal computation: arithmetic, function
 calls, etc.
 
-latexmath:[$\circ$] <<finish, Finish instruction>>: At this point the instruction pseudocode is done, the instruction cannot be restarted, memory accesses cannot be discarded, and all memory
+* <<finish, Finish instruction>>: At this point the instruction pseudocode is done, the instruction cannot be restarted, memory accesses cannot be discarded, and all memory
 effects have taken place. For conditional branch and indirect jump
 instructions, any program order successors that were fetched from an
 address that is not the one that was written to the _pc_ register are
@@ -552,15 +553,21 @@ them.
 
 Transitions specific to load instructions:
 
-latexmath:[$\circ$] <<initiate_load, Initiate memory load operations>>: At this point the memory footprint of the load instruction is
+[circle]
+* <<initiate_load, Initiate memory load operations>>: At this point the memory footprint of the load instruction is
 provisionally known (it could change if earlier instructions are
 restarted) and its individual memory load operations can start being
 satisfied.
-latexmath:[$\bullet$] <<sat_from_forwarding, Satisfy memory load operation by forwarding from unpropogated stores>>: This partially or entirely satisfies a single memory load operation
+
+[disc]
+* <<sat_from_forwarding, Satisfy memory load operation by forwarding from unpropogated stores>>: This partially or entirely satisfies a single memory load operation
 by forwarding, from program-order-previous memory store operations.
-latexmath:[$\bullet$] <<sat_from_mem, Satisfy memory load operation from memory>>: This entirely satisfies the outstanding slices of a single memory
+
+* <<sat_from_mem, Satisfy memory load operation from memory>>: This entirely satisfies the outstanding slices of a single memory
 load operation, from memory.
-latexmath:[$\circ$] <<complete_loads, Complete load operations>>: At this point all the memory load operations of the instruction have
+
+[circle]
+* <<complete_loads, Complete load operations>>: At this point all the memory load operations of the instruction have
 been entirely satisfied and the instruction pseudocode can continue
 executing. A load instruction can be subject to being restarted until
 the transition. But, under some conditions, the model might treat a load
@@ -568,44 +575,56 @@ instruction as non-restartable even before it is finished (e.g. see ).
 
 Transitions specific to store instructions:
 
-latexmath:[$\circ$] <<initiate_store_footprint, Initiate memory store operation footprints>>: At this point the memory footprint of the store is provisionally
+[circle]
+* <<initiate_store_footprint, Initiate memory store operation footprints>>: At this point the memory footprint of the store is provisionally
 known.
-latexmath:[$\circ$] <<instantiate_store_value, Instantiate memory store operation values>>: At this point the memory store operations have their values and
+
+* <<instantiate_store_value, Instantiate memory store operation values>>: At this point the memory store operations have their values and
 program-order-successor memory load operations can be satisfied by
 forwarding from them.
-latexmath:[$\circ$] <<commit_stores, Commit store instruction>>: At this point the store operations are guaranteed to happen (the
+
+* <<commit_stores, Commit store instruction>>: At this point the store operations are guaranteed to happen (the
 instruction can no longer be restarted or discarded), and they can start
 being propagated to memory.
-latexmath:[$\bullet$] <<prop_store, Propagate store operation>>: This propagates a single memory store operation to memory.
-latexmath:[$\circ$] <<complete_stores, Complete store operations>>: At this point all the memory store operations of the instruction
+
+[disc]
+* <<prop_store, Propagate store operation>>: This propagates a single memory store operation to memory.
+
+[circle]
+* <<complete_stores, Complete store operations>>: At this point all the memory store operations of the instruction
 have been propagated to memory, and the instruction pseudocode can
 continue executing.
 
 Transitions specific to `sc` instructions:
 
-latexmath:[$\bullet$] <<early_sc_fail, Early sc fail>>: This causes the `sc` to fail, either a spontaneous fail or because
-it is not paired with a program-order-previous `lr`.
-latexmath:[$\bullet$] <<paired_sc, Paired sc>>: This transition indicates the `sc` is paired with an `lr` and might
+[disc]
+* <<early_sc_fail, Early sc fail>>: This causes the `sc` to fail, either a spontaneous fail or becauset is not paired with a program-order-previous `lr`.
+
+* <<paired_sc, Paired sc>>: This transition indicates the `sc` is paired with an `lr` and might
 succeed.
-latexmath:[$\bullet$] <<commit_sc, Commit and propagate store operation of an sc>>: This is an atomic execution of the transitions <<commit_stores, Commit store instruction>> and <<prop_store, Propagate store operation>>, it is enabled
+
+* <<commit_sc, Commit and propagate store operation of an sc>>: This is an atomic execution of the transitions <<commit_stores, Commit store instruction>> and <<prop_store, Propagate store operation>>, it is enabled
 only if the stores from which the `lr` read from have not been
 overwritten.
-latexmath:[$\bullet$] <<late_sc_fail, Late sc fail>>: This causes the `sc` to fail, either a spontaneous fail or because
+
+* <<late_sc_fail, Late sc fail>>: This causes the `sc` to fail, either a spontaneous fail or because
 the stores from which the `lr` read from have been overwritten.
 
 Transitions specific to AMO instructions:
 
-latexmath:[$\bullet$] <<do_amo, Satisfy, commit and propagate operations of an AMO>>: This is an atomic execution of all the transitions needed to satisfy
+[disc]
+* <<do_amo, Satisfy, commit and propagate operations of an AMO>>: This is an atomic execution of all the transitions needed to satisfy
 the load operation, do the required arithmetic, and propagate the store
 operation.
 
 Transitions specific to fence instructions:
 
-latexmath:[$\circ$] <<commit_fence, Commit fence>>
+[circle]
+* <<commit_fence, Commit fence>>
 
 The transitions labeled latexmath:[$\circ$] can always be taken eagerly,
 as soon as their precondition is satisfied, without excluding other
-behavior; the latexmath:[$\bullet$] cannot. Although is marked with a
+behavior; the latexmath:[$\bullet$] cannot. Although <<fetch, Fetch instruction>> is marked with a
 latexmath:[$\bullet$], it can be taken eagerly as long as it is not
 taken infinitely many times.