diff --git a/apps/web/src/routes/kripke/+page.svelte b/apps/web/src/routes/kripke/+page.svelte index f443d79..b6af55e 100644 --- a/apps/web/src/routes/kripke/+page.svelte +++ b/apps/web/src/routes/kripke/+page.svelte @@ -3,24 +3,90 @@ import Katex from "$lib/components/katex.svelte"; import { type Formula, type Frame, + getFrame, + getId, + isomorphic, latexSymbols, prettyPrint, + validWorlds, } from "@cannorin/kripke"; import LuHeart from "lucide-svelte/icons/heart"; import LuHeartCrack from "lucide-svelte/icons/heart-crack"; import FormulaInput from "./formula-input.svelte"; import FrameInput from "./frame-input.svelte"; +import { getDailyFrame } from "./system"; let formula: Formula | undefined = $state(undefined); -let frame: Frame = $state({ relations: new Set() }); +let frame: Frame = $state(getFrame(0)); let math = $derived.by(() => { if (formula) return prettyPrint(formula, { symbols: latexSymbols }); return "\\phantom{p}"; }); -const life = 6; +const dailyFrame = getDailyFrame(); +const dailyFrameId = isomorphic[getId(dailyFrame)]; +let remainingRelations = $derived( + dailyFrame.relations.size - frame.relations.size, +); + +type Move = + | { type: "guess"; frameId: number; correct: boolean } + | { type: "check"; formulaStr: string; valid: number }; + +let moves: Move[] = $state([]); +let life = $derived(10 - moves.length); + +let canGuess = $derived.by(() => { + if (remainingRelations !== 0) return false; + const frameId = isomorphic[getId(frame)]; + return !moves.some( + (move) => move.type === "guess" && move.frameId === frameId, + ); +}); +function guess() { + if (!canGuess) return; + const frameId = isomorphic[getId(frame)]; + moves.push({ type: "guess", frameId, correct: frameId === dailyFrameId }); + moves = [...moves]; +} + +let canCheck = $derived.by(() => { + if (!formula) return false; + const formulaStr = prettyPrint(formula); + return !moves.some( + (move) => move.type === "check" && move.formulaStr === formulaStr, + ); +}); +function check() { + if (!canCheck || !formula) return; + const formulaStr = prettyPrint(formula); + const valid = validWorlds(dailyFrame, formula).length; + moves.push({ type: "check", formulaStr, valid }); + moves = [...moves]; + formula = undefined; +} +{#snippet sampleArrow()} + + + + + + + + +{/snippet} +

KRiPkE

@@ -38,24 +104,98 @@ const life = 6;
- +
+ id: {isomorphic[getId(frame)]} + + + {@render sampleArrow()} × {remainingRelations} + +
-
-
+ +
+ +
-
- Foo +
+

Rules

+
    +
  • + A Kripke frame with 4 worlds is generated. +
    • +
  • + The game tells you how many accessibility relations are in the frame, but not the exact shape of it. +
    • +
  • + You have a total of 10 moves (). + In each move you can do one of the following: +
      +
    • + Enter a modal formula. + The game tells you in how many worlds the formula is valid (for every valuation). +
      • +
    • + Guess the Kripke frame. + If your frame is equal or isomorphic to the secret frame, you win. +
      • +
    +
    • +
  • + You lose when you run out of moves. +
    • +
+ +

Syntax

+

You may use the following symbols:

+
    +
  • propositional variables: p, q, r, s
    • +
  • verum: T, ⊤, 1, \top
    • +
  • falsum: F, ⊥, 0, \bot
    • +
  • negation: ~, ¬, \neg, \lnot
    • +
  • box modality: [], □, L, \Box
    • +
  • diamond modality: <>, ⋄, M, \Diamond
    • +
  • conjunction: &, ^, ∧, \wedge, \land
    • +
  • disjunction: |, v, ∨, \vee, \lor
    • +
  • implication: ->, →, \rightarrow, \to, \implies
    • +
  • equivalence: <->, ↔, \leftrightarrow, \iff
    • +
  • parentheses: (, )
    • +
diff --git a/apps/web/src/routes/kripke/formula-input.svelte b/apps/web/src/routes/kripke/formula-input.svelte index 62adb1a..8732d4f 100644 --- a/apps/web/src/routes/kripke/formula-input.svelte +++ b/apps/web/src/routes/kripke/formula-input.svelte @@ -1,5 +1,5 @@ diff --git a/apps/web/src/routes/kripke/frame-input.svelte b/apps/web/src/routes/kripke/frame-input.svelte index 3a79387..e404a23 100644 --- a/apps/web/src/routes/kripke/frame-input.svelte +++ b/apps/web/src/routes/kripke/frame-input.svelte @@ -3,6 +3,7 @@ import { type Frame, type Relation, type World, + getFrame, left, reverse, right, @@ -11,27 +12,21 @@ import { import { type Vector, add, degree, rotate, sub, theta } from "./vector"; let { - frame = $bindable({ relations: new Set() }), + frame = $bindable(getFrame(0)), }: { frame?: Frame | undefined; } = $props(); -let relations = $state(new Set()); - -$effect(() => { - frame = { relations }; -}); - let selected: World | null = $state(null); function toggle(rel: Relation) { - if (relations.has(rel)) { - relations.delete(rel); + if (frame.relations.has(rel)) { + frame.relations.delete(rel); } else { - relations.add(rel); + frame.relations.add(rel); } // Reassign to trigger reactivity - relations = new Set(relations); + frame = { relations: new Set(frame.relations) }; } function handleNodeClick(node: World, event: MouseEvent) { @@ -59,24 +54,24 @@ function handleSvgClick() { const positions: Record = { a: { - x: 75, - y: 75, + x: 50, + y: 50, }, b: { - x: 225, - y: 75, + x: 200, + y: 50, }, c: { - x: 225, - y: 225, + x: 200, + y: 200, }, d: { - x: 75, - y: 225, + x: 50, + y: 200, }, }; -const center: Vector = { x: 150, y: 150 }; +const center: Vector = { x: 125, y: 125 }; const radius: Vector = { x: 20, y: 0 }; @@ -100,14 +95,14 @@ function getPath(rel: Relation) { const angle = theta(sub(positions[r], positions[l])); - const offset = relations.has(reverse(rel)) ? degree(10) : 0; + const offset = frame.relations.has(reverse(rel)) ? degree(10) : 0; const dl = rotate(radius, angle + offset); const dr = rotate(radius, angle + Math.PI - offset); const from = add(positions[l], dl); const to = add(positions[r], dr); - if (!relations.has(reverse(rel))) + if (!frame.relations.has(reverse(rel))) return `M ${from.x} ${from.y} L ${to.x} ${to.y}`; return `M ${from.x} ${from.y} C ${from.x + dl.x * 2} ${from.y + dl.y * 2}, ${to.x + dr.x * 2} ${to.y + dr.y * 2}, ${to.x} ${to.y}`; @@ -136,7 +131,7 @@ function getPath(rel: Relation) { - + - + - {#each Array.from(relations) as rel} + {#each Array.from(frame.relations) as rel} {#key rel} >> 16), 2246822507) ^ + Math.imul(h2 ^ (h2 >>> 13), 3266489909); + h2 = + Math.imul(h2 ^ (h2 >>> 16), 2246822507) ^ + Math.imul(h1 ^ (h1 >>> 13), 3266489909); + // Combine the two 32-bit hashes into a single 53-bit integer + return 4294967296 * (2097151 & h2) + (h1 >>> 0); +} + +export function getDailyFrame() { + // Use UTC ISO string so it's consistent across time zones + const dateStr = new Date().toISOString().split("T")[0]; + const hash = cyrb53(dateStr); + const index = hash % nontrivials.length; + return getFrame(nontrivials[index]); +} diff --git a/packages/kripke/semantics.ts b/packages/kripke/semantics.ts index 9cfcff4..db24b72 100644 --- a/packages/kripke/semantics.ts +++ b/packages/kripke/semantics.ts @@ -124,6 +124,7 @@ function applyPermutation( export function generateAllFrames() { const canonicals: number[] = []; + const nontrivials: number[] = []; const map = new Map(); const total = 2 ** relation.length; @@ -131,6 +132,7 @@ export function generateAllFrames() { if (map.has(id)) continue; const relations = decode(relation, id); + const frame = { relations }; const equivalentIds: number[] = []; @@ -148,6 +150,11 @@ export function generateAllFrames() { for (const equivalentId of equivalentIds) { map.set(equivalentId, canonicalId); } + + // Exclude the sizes with less than 10 frames (= can be bruteforced) + if (relations.size >= 3 && relations.size <= 13) { + nontrivials.push(canonicalId); + } } const isomorphic: Uint16Array = new Uint16Array(total); @@ -157,8 +164,18 @@ export function generateAllFrames() { isomorphic[id] = value; } - return { canonicals, isomorphic }; + return { canonicals, isomorphic, nontrivials }; } -const { canonicals, isomorphic } = generateAllFrames(); -export { canonicals, isomorphic }; +const allFrames = generateAllFrames(); + +/** canonical frames among all the isomorphic ones */ +const canonicals = allFrames.canonicals; + +/** mapping to get the canonical frame */ +const isomorphic = allFrames.isomorphic; + +/** frames that are suitable for the puzzle */ +const nontrivials = allFrames.nontrivials; + +export { canonicals, isomorphic, nontrivials };