kripke: refactor (2)
This commit is contained in:
3
.vscode/settings.json
vendored
3
.vscode/settings.json
vendored
@@ -21,5 +21,6 @@
|
|||||||
},
|
},
|
||||||
"[jsonc]": {
|
"[jsonc]": {
|
||||||
"editor.defaultFormatter": "biomejs.biome"
|
"editor.defaultFormatter": "biomejs.biome"
|
||||||
}
|
},
|
||||||
|
"biome.lspBin": "./node_modules/@biomejs/biome/bin/biome"
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -62,7 +62,7 @@ onMount(() => {
|
|||||||
<li>You can also play <a href="/kripke/random">Random Challenge</a>.</li>
|
<li>You can also play <a href="/kripke/random">Random Challenge</a>.</li>
|
||||||
</ul>
|
</ul>
|
||||||
|
|
||||||
<Rules />
|
<Rules relationSize={relationSize} />
|
||||||
</section>
|
</section>
|
||||||
</div>
|
</div>
|
||||||
</main>
|
</main>
|
||||||
|
|||||||
@@ -48,7 +48,9 @@ let formula: Formula | undefined = $state(undefined);
|
|||||||
let formulaStr = $derived(
|
let formulaStr = $derived(
|
||||||
formula ? prettyPrint(formula, { symbols: latexSymbols }) : "",
|
formula ? prettyPrint(formula, { symbols: latexSymbols }) : "",
|
||||||
);
|
);
|
||||||
let frame: Frame = $state(getFrame(0));
|
let frame: Frame = $state(
|
||||||
|
getFrame(moves.findLast((move) => move.type === "guess")?.frameId ?? 0),
|
||||||
|
);
|
||||||
let frameId = $derived(getId(frame));
|
let frameId = $derived(getId(frame));
|
||||||
|
|
||||||
let remainingRelations = $derived(relationSize - frame.relations.size);
|
let remainingRelations = $derived(relationSize - frame.relations.size);
|
||||||
|
|||||||
@@ -2,8 +2,11 @@
|
|||||||
import Katex from "$lib/components/katex.svelte";
|
import Katex from "$lib/components/katex.svelte";
|
||||||
import LuHeart from "lucide-svelte/icons/heart";
|
import LuHeart from "lucide-svelte/icons/heart";
|
||||||
|
|
||||||
|
let { relationSize }: { relationSize: number } = $props();
|
||||||
|
|
||||||
const frame = "\\footnotesize \\mathcal{F} = \\left<W, R\\right>";
|
const frame = "\\footnotesize \\mathcal{F} = \\left<W, R\\right>";
|
||||||
const numberConstraint = "\\footnotesize |W| = 4";
|
const worldConstraint = "\\footnotesize |W| = 4";
|
||||||
|
const relationConstraint = `\\footnotesize |R| = ${relationSize}`;
|
||||||
const f = "\\footnotesize \\mathcal{F}";
|
const f = "\\footnotesize \\mathcal{F}";
|
||||||
const validCount =
|
const validCount =
|
||||||
"\\footnotesize \\mathrm{N}(\\varphi) = \\bigl| \\Set{ w \\in W | \\forall \\mathop{\\Vdash}\\, (w \\Vdash \\varphi) } \\bigr|";
|
"\\footnotesize \\mathrm{N}(\\varphi) = \\bigl| \\Set{ w \\in W | \\forall \\mathop{\\Vdash}\\, (w \\Vdash \\varphi) } \\bigr|";
|
||||||
@@ -12,11 +15,8 @@ const validCount =
|
|||||||
<h2>Rules</h2>
|
<h2>Rules</h2>
|
||||||
<ul>
|
<ul>
|
||||||
<li>
|
<li>
|
||||||
A Kripke frame with 4 worlds is generated:
|
A <a href="https://en.wikipedia.org/wiki/Kripke_semantics" target="_blank" rel="noopener noreferrer">Kripke frame</a> with 4 worlds and {relationSize} relation(s) is generated:
|
||||||
<Katex math={frame} />, where <Katex math={numberConstraint} />.
|
<Katex math={frame} />, where <Katex math={worldConstraint} /> and <Katex math={relationConstraint} />.
|
||||||
</li>
|
|
||||||
<li>
|
|
||||||
The game tells you how many accessibility relations are in the frame <Katex math={f} />, but not the exact shape of it.
|
|
||||||
</li>
|
</li>
|
||||||
<li>
|
<li>
|
||||||
You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>.
|
You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>.
|
||||||
@@ -32,7 +32,7 @@ const validCount =
|
|||||||
</li>
|
</li>
|
||||||
<li>
|
<li>
|
||||||
Guess the Kripke frame.
|
Guess the Kripke frame.
|
||||||
If your frame is equal or isomorphic to the secret frame <Katex math={f} />, you win.
|
If your frame is equal or isomorphic to <Katex math={f} />, you win.
|
||||||
</li>
|
</li>
|
||||||
</ul>
|
</ul>
|
||||||
</li>
|
</li>
|
||||||
|
|||||||
@@ -50,13 +50,13 @@ $effect(() => {
|
|||||||
<section class="w-[300px] prose prose-sm">
|
<section class="w-[300px] prose prose-sm">
|
||||||
<h2>Random Challenge!</h2>
|
<h2>Random Challenge!</h2>
|
||||||
<ul>
|
<ul>
|
||||||
<li>The answer of the game is determined by a seed number {@render seedNumber()}, which changes on every reload.</li>
|
<li>The answer of the game is determined by a seed number {@render seedNumber()}.</li>
|
||||||
<li>You can right-click on the seed number to obtain a permalink to this exact game.</li>
|
<li>You can right-click on the seed number to obtain a permalink to this exact game.</li>
|
||||||
<li>Unlike Daily Challenge, the progress of the game does not persist.</li>
|
<li>Unlike Daily Challenge, the progress of the game does not persist.</li>
|
||||||
<li>You can also play <a href="/kripke">Daily Challenge</a>, if you have not yet.</li>
|
<li>You can also play <a href="/kripke">Daily Challenge</a>, if you have not yet.</li>
|
||||||
</ul>
|
</ul>
|
||||||
|
|
||||||
<Rules />
|
<Rules relationSize={relationSize} />
|
||||||
</section>
|
</section>
|
||||||
</div>
|
</div>
|
||||||
</main>
|
</main>
|
||||||
|
|||||||
Reference in New Issue
Block a user