The state edge¶
The state edge, true on the step a bool turns true: true now and false as the step began, once on each turning true, never while it holds, never as it falls.
Events are lists: a game's own binding appends to its list where rose holds. Named rise, not edge, a word of the grammar. Source: events are lists, so the state edge is a kernel of its own. Checked against a reference in numpy, which has its own tests.
- Source
- lusine's rule; the edge-triggered event of 5933833092, which it replaces.
- Proof
- invariant, limit.
rise.trait
namespace lusine.events;
bool rise(bool signal)
{
return signal && !previous(signal);
}
True on the step a bool turns true, rose = signal && !previous(signal), the signal now and as the step began. Events are lists: a raise is an append, and the game's own binding appends to its list where rose holds; Boules, for example, appends to landings where a ball's landed rose.
import os, sys
root = os.getcwd()
while not os.path.isfile(os.path.join(root, 'docsite.json')):
root = os.path.dirname(root)
sys.path.insert(0, os.path.join(root, 'tools'))
import numpy as np
import matplotlib.pyplot as plt
from lusine import trait_run
EPS = float(np.finfo(np.float32).eps)
The kernel¶
The law as the library states it, and as this page runs it.
print(trait_run.source('events/rise.trait'))
// lusine.events.rise: the state edge, true on the step a bool turns true: true now and false as the step began, once
// on each turning true, never while it holds, never as it falls. Events are lists: a game's own binding appends to
// its list where `rose` holds. Named `rise`, not `edge`, a word of the grammar.
// Source: events are lists, so the state edge is a kernel of its own.
// Checked against a reference in numpy, which has its own tests.
namespace lusine.events;
bool rise(bool signal)
{
return signal && !previous(signal);
}
The program¶
A signal is a game's own bool, written in the step; previous reads it as the step began. Here the host sets each item's run of 32 steps once, as the bits of a word (trace, bit t the signal in step t), and the program's own kernels read the step's bit and count the steps; then the library's kernel finds the edge. Before the first step every signal is false, so a signal true from the first step rises there. Every item runs in one program, 32 steps, each step's signal and rose read back.
EDGE = """namespace edge;
lusine.version version = { { number = 1 } };
struct item { bits trace; integer ticks; bool signal; bool rose; };
lattice<item, 1> items(spacing = 1 m, boundary = wall);
bool sensed(bits trace, integer ticks) { return ((trace >> ticks) & bits(1)) == bits(1); }
integer tick(integer ticks) { return ticks + 1; }
void main()
{
items.signal = sensed(items.trace, items.ticks);
items.rose = lusine.events.rise(items.signal);
items.ticks = tick(items.ticks);
}
"""
print(EDGE)
HAND = [0, 0, 1, 1, 1, 0, 1, 0, 0, 1, 1, 0]
CASES = {'hand': HAND, 'held true': [1] * 32, 'held false': [0] * 32, 'falling': [1, 1, 1] + [0] * 29}
rng = np.random.default_rng(3)
words = [sum(bit << t for t, bit in enumerate(c)) for c in CASES.values()]
words += [int(w) for w in rng.integers(0, 2 ** 32, 200, dtype=np.uint64)]
run = trait_run.Program(['events/rise.trait'], EDGE, {'edge.items': [len(words)]})
run.store('edge.items', 'trace', words)
signal, rose = (a.astype(bool) for a in run.steps('edge.main', 32, [('edge.items', 'signal'), ('edge.items', 'rose')]))
before = np.vstack([np.zeros((1, len(words)), bool), signal[:-1]]) # each step's signal as it began
assert np.array_equal(signal, (np.array(words, dtype=np.uint64)[None, :] >> np.arange(32, dtype=np.uint64)[:, None]
& np.uint64(1)).astype(bool))
namespace edge;
lusine.version version = { { number = 1 } };
struct item { bits trace; integer ticks; bool signal; bool rose; };
lattice<item, 1> items(spacing = 1 m, boundary = wall);
bool sensed(bits trace, integer ticks) { return ((trace >> ticks) & bits(1)) == bits(1); }
integer tick(integer ticks) { return ticks + 1; }
void main()
{
items.signal = sensed(items.trace, items.ticks);
items.rose = lusine.events.rise(items.signal);
items.ticks = tick(items.ticks);
}
Invariant: once on each turning true¶
Over a signal's run the rises are exactly its turnings from false to true: none while it holds, none as it falls.
r = rose[:len(HAND), 0]
assert r.tolist() == [False, False, True, False, False, False, True, False, False, True, False, False], r
fig, ax = plt.subplots(figsize=(7, 2.2))
ax.step(range(len(HAND)), signal[:len(HAND), 0], where='post', label='signal')
ax.plot(np.nonzero(r)[0], np.ones(int(r.sum())) * 1.1, 'v', label='rose')
ax.set_yticks([0, 1]); ax.set_xlabel('step'); ax.legend(loc='lower right')
plt.show()
Invariant: two hundred random signals¶
Over 200 random signals of 32 steps, each step's rise is the signal now and not as the step began, item by item, and the rises number the signals' turnings true.
r, s, b = rose[:, 4:], signal[:, 4:], before[:, 4:]
assert np.array_equal(r, s & ~b)
assert int(r.sum()) == int(np.sum(s & ~b)) and not np.any(r & ~s)
print(int(r.sum()), 'rises over', s.size, 'item-steps')
1658 rises over 6400 item-steps
Limit: held or falling, it never rises again¶
A signal held true rises once, on its first step, from the start's false, and never while it holds; one held false never rises; one falling never rises as it falls.
held, never, falling = rose[:, 1], rose[:, 2], rose[:, 3]
assert held.tolist() == [True] + [False] * 31
assert not never.any() and falling.tolist() == [True] + [False] * 31
print('held true: one rise, on the first step; held false and falling: none after')
held true: one rise, on the first step; held false and falling: none after