[ home / rules / faq / search ] [ overboard / sfw / alt ] [ leftypol / edu / labor / siberia / lgbt / latam / hobby / tech / games / anime / music / draw / AKM / ufo / 420 ] [ meta ] [ wiki / shop / tv / tiktok / twitter / patreon ] [ GET / ref / marx / booru ]

/tech/ - Technology

"Technology reveals the active relation of man to nature" - Karl Marx
Name
Options
Subject
Comment
Flag
File
Embed
Password(For file deletion.)

Check out our new store at shop.leftypol.org!


File: 1726459786963.png (365.18 KB, 709x538, nuimageboard.png)

 

The neverending quest to rewrite vichan -

Archived threads:
https://archive.is/xiA7y
249 posts and 59 image replies omitted.

>>31483
>This is turning out to be a little more significant than first envisioned.
Got the endpoints rewritten and am most the way through with the models.
As usual its the moderation related functionality that are giving the most trouble.
Further need to rework the related posts endpoint to be able to handle range bans.

>>31487
>Got the endpoints rewritten and am most the way through with the models.
>As usual its the moderation related functionality that are giving the most trouble.
>Further need to rework the related posts endpoint to be able to handle range bans.
Finished off the endpoints and the models, had to add back References.

An advantage of ">>thread/post" syntax is that you can shard on board without querying across shards.
This is because the parser no longer needs to query for the thread of the post to link.
However with snowflakes this would be 22 or 24 characters long, which is unreasonable.
Further removing this step from the parser also removes the validation of cross-thread links.

We could mangle the endpoint such that /{board}/res/{post} returns the relevant /{board}/res/{thread}.
The front-end would then be responsible for translating to the canonical /{board}/res/{thread}#{post}.
Since it's already an SPA this wouldn't be the biggest deal, but is ugly, and removes cross-thread link validation.
The validation isn't as big a deal as the ugliness to me.

Trips are another problem in need of a solution…

>>31495
>We could mangle the endpoint such that /{board}/res/{post} returns the relevant /{board}/res/{thread}.
Made the backend require an SPA or complex DOM operations in the front-end by making links unusable without JavaScript.
The reason was to make sharding by board trivial, avoiding the parser having to query for post threads to form URLs.
Corrected my error and decided returning a correct output for the user was more valuable than more efficient sharding.
At present whatever handles the front-end just has to be capable of fetching/manipulating JSON, and concatenating strings.
Rendering the HTML contained in the JSON in native apps isn't much more complicated given existing libraries.

Regarding the HTTP header waste caused by having each post be requested separately rather than a bulk endpoint.
For an English language textboard waste could be as high as 10%, but for an imageboard more like 1%.
But this is waste that doesn't touch the server since all the posts are sent from the CDN to the client.
I'm worried about cache poisoning when hosted without a CDN or without cloudflare;

>>31497
It feels like the API is starting to solidify.
Only successful API changes of the last several were:
- Replacing the offset with a cursor.
- Allowing for address ranges in the related posts.
Am working on the queries presently.
Completed the thread, and catalog queries.
Even optimized them a little, though don't really know how.
Was pretty weak today, and didn't get much out of bed.
So the rest of the queries are going to probably wait.

>>31503
>So the rest of the queries are going to probably wait.
Managed to get a few more similar queries done:
So now there are trip, related, and report queries.
This included setting up IP range queries for the related page.
These work without exposing the IP to the moderator.
Especially helpful if there are ever user created boards.
Also compressed down the JSON for the post metadata.
The vast majority of the data here is null.
So we just remove the empty elements.

>>31506
Am interested in transforming this into a federated platform with "little boxes".
There are mandatory trips where the trip password is a edDSA private key and the trip a public key.
These are generated client side, and the private key never hits the wire let alone the server.
Usernames are equal to the public key, unless the user changes them.
The client signs the HTTP packet client side that will be sent to the outbox of the post it responds to.
There are group actors of different kinds which make up the boards.
We accept all follows and drop all DMs to keep things simple and safe.

>>31508
>Am interested in transforming this into a federated platform with "little boxes".
There are three problems with this:
1. Fediverse UI assumes one repliee per post.
2. There are caching and scaling difficulties with ActivityPub.
3. ActivityStreams are complicated.

Fortunately 1. is a small percentage of posts.
Probably less than 5% are of a form that can't be easily broken up or changed for an @mention.
In the absolute worst case you should still be able to link to posts using the URL.
Still not sure about what the UI for this should be. [^1]

Seems the standard issue scaling solution is making everything maxage=300 JSON plus a CDN.
The Inbox is a POST endpoint, and so can't be cached, but there is sharedInbox which makes it a little easier.
Being focused on Group with anonymous users should prevent the feed, and search related performance drains.

Sounds like a ton of work if not another complete rewrite…

Unrelated but ended up combining WikiMedia, Markdown, and old Reddit markup to make a hybrid that seems to work well:
Wikimedia: labeled external URLs, and italics
Markdown: quotes, bold, underline (sort of anyway), strike, code
old-Reddit/StackOverflow: spoilers

wikimedia_external_link = (string("[") >> url << string(" ")) + \
    formats_without_urls.until(string("]")) << string("]").map(
        lambda url, label: LabeledURL.model_validate({ "url": url, "content": label })
    )

pre = (string("```") >> pretext << string("```")).map(
    lambda c: (make_code(c)).model_validate({ "content": c })
)

quote = (regex(r"(^|\n|\r)>") >> formats.until(regex("(\n|\r|$)"))).map(Quote)

spoiler = balanced(">!", "!<", Spoiler)
strike = balanced("~~", "~~", Strike)
italic = balanced("''", "''", Italic)
bold = balanced("**", "**", Bold)
underline = balanced("__", "__", Underline)

This is bound to be confusing, so I'm going to have a popup on first login show the format and rules.

:[^1] Might be misremembering this but seem to recall a web forum with parent child color correspondence.
So each post is assigned two colors, one as a parent and one as a child and if the child-parent color and parent-child color match they are related.
This keeps the replies flat (there's only ever two color blocks) while still having a visual graph.
You could also have multiple views for chronological versus replyTo chronological sorts.
We keep post preview on hover also, which is a real quality of life improvement for non-local replies.
Then again maybe this is strictly worse than just using the SnowflakeID…

>>31540
Less gibberish, important bits:
- Keep private keys off the wire/server.
- Cache immutable the outbox.
- Use sharedInbox.
- Use a CDN for caching.

Also with https://github.com/joewlos/activitypubdantic instead of "little boxes".
And further drop any strange pagination requests to the outbox.

>>31541
Thought of a couple more ways to improve performance.
- Use workers for fanout of POST requests in server-to-server.
- Use NoSQL for storage of ActivityPub.

Am using Beanie in this 2.2, and the question is, "is this an added translation layer".
There is imperfect translation between Beanie and PyMongo Async queries.
This goes against a design principle that was working so excellently in 2.1.
And this is a little disappointing.

The plus-side is managed to make it economical to scale since it's 0.30 USD / 1m requests.

>>31541
>Cache immutable the outbox.
I wrote signature verification for the inbox and three implementation for the Person outbox.
Think I'd like it to be illegal to use an irregular cursor/page so that the cache rarely misses.
But would also like to avoid using the "skip" parameter with O(n) search of the documents.
No matter how it's implemented it seems to require a document mapping cursors to pages.

>>31548
Settled on just using a cursor and "trusting" that servers won't use irregular cursors.
Or else that it may be possible to remove services which query the origin excessively.

Further this is a singly linked implementation because Delete and Update are included.
Delete and Update requires that the pages be traversed in full to render next elements.

The first page is always the total_items modulo the config.OUTBOX_PAGE_SIZE.
This allows every subsequent page to be cached immutable so long as the linked cursors are used.

We also drop the "partOf" parameter to avoid making the full (mutable) collection.

It's all above board with the spec too.
Only downside is the mentioned "trust" required of servers.

Wrote the Person following and followers endpoints.
Ended up not materializing the document to keep track of this.
So similar to the outbox this is just a query on the ActivityModel class.
The only real advantage to this is in bookkeeping.
It's slow because it's not really possible to cache these pages.
It should be less than 50ms (maybe less than 10ms on heavy hardware), for a page, which is probably too slow.
There is also a precondition that there be one follow not undone for any thousand.
This is to make it computationally feasible.

>>31567
It's a bit of a fail to write a federated server with mongodb in anything but typescript.
Guess there's going to be a 2.3 using fedify, mongodb, and typescript.
Think need to separate out the Activity logs from the materialized views.
This is to make the follwers, following, and like sufficiently performant.
My impression is that the client to server protocol would make things like bump ordering difficult.
So there probably needs to be a third layer to the API for a cache efficient client.

>>31583
For future reference, the private key idea is to use fordwardActivity() [^1].
And simply sign on the client side for all the relevant servers sent via a separate endpoint.
It's apparently trivial to wrap the existing fedify classes as monogodb documents with indices.
For the POST fanout use fedify/x/cfworkers [^2] including POSTing to the origin…

:[^1] https://fedify.dev/manual/inbox#forwarding-activities-to-another-server
:[^2] https://github.com/fedify-dev/fedify/pull/242

I thought of a way to simplify this project following in line with existing federated imageboard: Just make the Group the owner of Notes and Articles posted to anonymously to the board.

How loosely is your federation coupled and do you try to solve the problem of link rot in any way? Seeing this thread again made me want to take a crack at the personal wiki/bbs fusion idea, which i might specify a non-turing complete "link description language" for, that should enable users to do anything from replicating immutable resources within instance resource limits to controlling the display and pruning order of replies.
>>31291
>So if you make an Article instead of a Note you get unlimited length and HTML tags because you just link back to your instance in the feeds.
Is this the basis of your federation model, or do you replicate anything besides metadata?

>>32216
As far as the tool for thought first described in >>31282 goes, I'm not sure you could have the Group be the Actor writing the Notes and Articles, and simultaneously have something like user microblogs. Mainly because there would be no way to follow. These are really separate applications.

>>32223
Not if you combine everything into a comprehensive indexing system based on links to immutable data. You could totally have a serious of imageboard-style posts rendered as a twitter-style thread, which you would then curate on your "user" page.

>>32232
Your first sentence is correct, but I don't understand how you could curate the "user" page with Persons relegated to a foreign concept. Doing it by IP is both inaccurate, a security threat, and potentially reintroduces identity. Perhaps you could have a more sophisticated semantic tagging approach - hashtags and similar? Even automatically assigned by an LLM? What do you think?

>>32246
As i said above, secure tripcodes are entirely accurate for defining a user identity. The only problem with that would be human-readable unique names, for which there would be no way to ensure fair allocation without sacrificing anonymity. Maybe on a transient node you could have nicknames, that are unassigned when anything attached to the identity has been pruned.

>>32251
A secure trip could be a Person. My understanding is you could use name for the display name with preferredUsername set to the secure trip which is "unique". Then just default the name to "Anonymous" or the user selected name.

I kept getting bogged down before in my dislike of in effect having two different account systems: one username, and password pair for moderation (session based - in part for protected views), and a (optional) trip, and password pair (form based) for posting.

An advantage of the tags over board approach is that it makes clear which Group is posting, the only one that exists locally, if you want to reach out into the rest of the fediverse for posting. This is orthogonal to your attempts to create a Person.

>>32256
>I kept getting bogged down before in my dislike of in effect having two different account systems: one username, and password pair for moderation (session based - in part for protected views), and a (optional) trip, and password pair (form based) for posting.
I guess the merger we've just been discussion is roughly that there could be session based accounts for Actors (how you get a trip) and deletion passwords for posts, with the password hash. You can delete or edit either by the post password hash or by the session login.

>>32256
>you could use name for the display name with preferredUsername set to the secure trip which is "unique"
In the general case there are normalfags on the site, which wouldn't want to link to user pages by a tripcode.
>An advantage of the tags over board approach is that it makes clear which Group is posting, the only one that exists locally, if you want to reach out into the rest of the fediverse for posting.
In my planned approach boards are immutable, supersedable anchors, that allow threads to link to them. Therefore a different instance could create a post linking to a board or a thread (anything allowing replies) and every node in sync will render it on the board in accordance with the implicit graph structure.

In this case unstructured, tagged posts should probably only be propagated on small nodes or use a local tag, which may be shown as a "timeline".

>>32258
>for normalcomards
Well, you're right this isn't ideal. Mentions would be uglier even if you had autocomplete from follows/thread actors and info onmouseover.

>immutable, supersedable anchors, that allow threads to link to them

Excellent. But is it simpler, and more interoperable than just having a custom of mutual following for Group actors?

>>32259
>custom of mutual following
I don't think follows should be part of the protocol. My scheme would use replication structure i.e. readers are either downstream nodes or exposed out-of-band by another node. Prose is highly redundant, so i think native lz4 compression would prevent even a several decade-old network run on top of the protocol from reaching the same multi-terabyte data sizes as usenet. If storage size was to blow up though, node admins should still be able to pivot to a more frugal replication policy, like most activitypub instances have by design.

>>32261
>I don't think follows should be part of the protocol. My scheme would use replication structure i.e. readers are either downstream nodes or exposed out-of-band by another node.
I don't fully understand, and admittedly my abilities to implement complex programs are limited, if this would in fact be one.

>native lz4 compression

This is an important point. I believe you can do this for postgres rows.

I do now have a program (technically called "arsvia-redux") which has the creation of Person objects for login and signup using HTMX, sessions, and CSRFTokens. It needs testing, review, and revision. I'm not sure I really have the energy to dedicate to it or not.

>>32268
It seems like eventually the AI will be better even at Marxist analysis than experts. I'm very interested in making a censor. It's a bit of a stretch goal with this project, even if Llama Guard is central. I don't feel exactly qualified to make it. Censoring chauvanist content and policies seems obvious since it's so prevalent. The truth is that there are so many errors possible, and some of them are so subtle. It seems almost impossible to censor them all.

>>32279
>AI will be better at Marxist analysis than experts
It can be useful at flagging things for human review, but please don't drink the AGI koolaid. LLMs are fundamentally incapable of reliably performing tasks outside their "training" data.
>>32268
>I don't fully understand, and admittedly my abilities to implement complex programs are limited, if this would in fact be one.
To get around the limitation of immutable records, child records ("scions") will reference a field of an existing record ("stock") and on sync get added to a mutable substructure ("shadow") of the stock. This means requesting scions will only turn up records present on a particular node, but it also means networks have an interest in propagating as much metadata and inline data as possible to every node.

>>32280
>It can be useful at flagging things for human review, but please don't drink the AGI koolaid. LLMs are fundamentally incapable of reliably performing tasks outside their "training" data.
Llama Guard 4 still has 11% false positive rate, but I think eventually this would be low enough to serve as a filter for content without moderator intervention, this is actually critical to the design because federation makes CIDR bans impractical.

Perhaps I'm getting habituated to the trolls here, but after the spam, and since the plan is to be text only, part of me is even more interested in censoring wrong thinking than illegal content. Yet I've no idea how to formulate such a censor.

The point wouldn't be to create a hugbox, where there was strict decorum, and you couldn't call each other uyghur or whatever. There's still plenty of disagreement among the left, and analysis to current events to talk about. So what is the point? I guess the idea is just to at once allow for outreach to a larger community without being overwhelmed by wrong thinking.

This is related to the follow-follow model I proposed. If the Group follows any Actor that follows the Group, and you allow users to act as the Group with other Actors (perhaps there's an account to make a user feed, but they can still post as the Group - and these posts then show up in the Group feed) you can get outreach without having the main page filled with wrong thinking.

>>32282
>Yet I've no idea how to formulate such a censor.
My best guess is that the best way to formulate this censor is not by ahead of time trying to think of an exhaustive set of rules but by labeling the dataset and having the machine derive the prompt ala: https://dspy.ai/#2-optimizers-tune-the-prompts-and-weights-of-your-ai-modules This would be a lot of work.

I've made a repository for this federated rewrite, in case anyone is interested: https://codeberg.org/jugaad/arsvia-redux so far it has the basic machinery for the creation of Person objects, session management (>>32268), and the improved (>>31540) parser, with a lot of tests.

I'm thinking presently that the moderation would be a challenge. I really hate thinking about this stuff let along actually managing a site. With PhotoDNA, URL rules, and word filters might be possible to remove the most offensive content. Llama Guard can catch some other junk, but there's no human out of the loop solution that exists today, and that there are no accounts, and federation (without federated CIDR lists) makes any sort of bans effectively impossible.

>>32438
Anyone have any ideas what to do about bans?

>>32439
Have been working to try to get the Note/Article/Page TABLE setup, and the subsequent catalog view. Am just using picoCSS at the moment but pics rel. are what things look like right now.

>>32439
When all else fails, make users keep a killfile! Vichan can hide by name, which is obviously of limited utility when anonymity is concerned, so maybe also implement basic glob or regex filters.

>>32455
>so maybe also implement basic glob or regex filters.
Filters are certainly what I was considering, but in a central censor to allow for more costly filters. Perhaps these could be togglable by the user to give a similar effect to the decentralized glob and regex filters. Obviously these posts wouldn't be federated, and would either be made hidden or removed.

The trouble is that I'm not sure the bots can do a good enough job. There are just so many ways to manipulate a conversation in a negative direction COINTELPRO - or even folks who do this work for free. I think I read that even detection of hate speech is something like a 70% accuracy affair for Facebook with much more developed tools at their disposal, and we're looking to detect far more subtle acts than hate speech.

I'm really at a loss for how to manage this, and it might be hindering my motivation to progress.

>>32461
Think there's really only two design objectives:
1. equal power to every post/poster
- no follower/following model.
- no ranking of posts by popularity.
- no names to discriminate content of users.
- (optional: following based on content via tags.)
2. quality content.
- access to a large collection of posts (federation - you could always make a new server but not you can get content on it).
- some restriction on the domain of acceptable discourse.

The fundamental contradiction is that without CIDR (centralization - and so no content) or usernames (reputation - and so unequal power) to distinguish posters I think there is no possibility of any sort of bans, and this makes creation of quality content difficult with today's level of technology.

>>32461
>a central censor to allow for more costly filters
Filters shouldn't be costly, unless there's something deeply wrong with your architecture (like emacs gnus scoring articles in a single thread by fetching them multiple times).
>The trouble is that I'm not sure the bots can do a good enough job.
They likely can't. This is why you give users the options to configure these filters, because it allows them to do aggressive filtering at their own risk. The more a filter or lack thereof bothers them personally, the more time they will spend on refining it, a textbook case of worse-is-better.

>>32471
>Filters shouldn't be costly.
Well, if we're using LLMs at all they would be from the user perspective.

>They likely can't. This is why you give users the options to configure these filters, because it allows them to do aggressive filtering at their own risk.

This tracks, it's a good idea. Having two tiers of filtering, one for basic federation (meeting basic social standards of the fediverse) and another tier with per instance filtering you could make it federate well, at least on the level of the Group. I also like the idea that sense we're working with trees of a single inReplyTo link per post you can go ahead and hide entire trees at once. Making bump ordering work with this is a tractable problem.

Went ahead and got the creation of Note and Article objects, and the display of the catalog done today with the help of "opencode". No file attachments at the moment of thread pages. Had to replace the >!spoiler!< syntax with the more contemporary ||spoiler|| so that the quotes would parse correctly.

Today had opencode add the thread posts, I didn't really like the way it structured the model code so I had to fix this.

Had another idea: a "difficult" POW for newly created accounts. This is roughly equivalent to banning everyone by default and having a default ban length. With this you could have actual user Actors instead of just the Group, but purely optional usernames, and still have bans that make some sense. Sort of think I no longer have the energy to dedicate to this project. Might just wait for the LLMs to get good enough to write this themselves.

Reincarnating this project once again.
Another cycle around the wheel.
Some interesting technical deviations.
Post-modernist feature set planned.
Skepticism of synthesizing the negated.
Leaving the unnegated pieces whole.
Designing to leave nothing behind.
Pragmatic enough to be completed.
Performance somewhat lacking.

Islands from Deno/Fresh.
Repos injected into functional cores.
Design to test, though I haven't yet.
MongoDB instead of translation or SQL.
Zod for schemas, and form validation.
A similar datatype used throughout for error reports.
Controlling for invariant and reporting errors.
Fedify worth it enough to change the whole stack.

https://codeberg.org/jugaad/anatta

Drafted a two-thirds page "spec", and stepwise "plan" for implementation of Group Person interactions. It's closer to what you'd use for a shed, than for the golden gate bridge, still way better than what have been doing. The only trouble which seems legitimate was that for threadiverse Groups to receive inReplyTos you have to Follow. The solution to this is that you can't Undo Follows, because this would break listening for inReplyTos, and so we replace it with a toggle for various visibilities. You also must Follow in order to Create(Note) on these other communities, which is not so bad.

guess tor is kill, rip; imagine how bad it would be if this site was compromised…

I didn't want to post this yet as the projects still in infancy.
But here's a somewhat topical list of features planned:
  • Follows and feeds (including for remote).
  • federated cross-posts a la >>33832 (You)
  • option for Group's which can post as the Group without login.
  • tags on Groups.
  • granular per tag moderator permissions.
  • "invisible" local karma (HN algo. sorting)
  • LLM rewriting of posts.
    • raw site with original Notes.
    • cooked site with rewritten, and click to raw view.

  • tor posting with email verified accounts.
  • websockets for liveboard.
  • pagenated CDN caching.
  • a real parser LL(\infinity).

I'm fairly happy with the feature set, am open to critique.

Have been working on the "spec" for the handle page.
It's split into a number of endpoints with several layers.
It's turned out to be relatively simple, but different than the initial implementation

  • profile.tsx
    • Initial query for Actor.
    • onScroll getCollectionService for page (in Island)
    • If the end is visible WebSockets for further data (in Island)

  • getActorService
    • Returns an Actor, and isAnonymous.
    • uses getObject, and caches to Redis.
    • CDN caches for with TTL.

  • getCollectionService (also used for replies, and Follows)
    • Returns a OrderedCollectionPage
    • Caches page data in Redis
    • "Reconstructs" the OrderedCollectionPage with cursor.
    • First page made with length modulo pageSize. (to standardize page boundaries)
    • CDN caches for with TTL.

  • postFollowService (reply and like/dislike are similar)
    • Get the necessary data from the database, and cookiePrinciple.
    • Create the Follow in DB.
    • Issue Create to recipient.



The rate limits and (granular) permissions are going to be handled by the _middleware.ts.
The rate limits are going to be by account or IP whichever is larger.

The only other big federated view is going to be the thread view which is going to use FEP-f228.

>>33832
I believe I've thought of a more elegant, if more resource heavy "spec."
Direct inReplyTos are almost always sent to the attributeTo if I understand correctly.
You then need only look up the context for each of these to get their replies.
With this you can then cache and regenerate the cache as needed with TTL.

Lemmy, and probably other instances don't issue 304 for their API endpoints, which means it has to be pummeled just to check for collection update. They also fail to use stable page boundaries, meaning you have to pummel every preceding page to get what you're after. An OrderedCollectionPage really seems like it should be organized as the N pages: {null, N-1, .. 1} with a 304, so that insertions never invalidate the cache except for the null page, and deletions only invalidate either one page or pages "to the left," if you care about fragmentation. The only downside is that queries are less efficient than when using a cursor, but this likely matters much less than not serving pages, especially when behind a CDN.

I've been writing a proxy for these OrderedCollectionPages which serves them correctly for use by the client. It still needs some work. One of my goals was to do this without actually caching any data on the server to keep memory usage low, leaving everything up to the CDN. Unfortunately the algorithm as implemented has a fatal error:
  1. We throw out all the data except for what's need for the newPage. (!)

  • In doing so we fail to update any case where updated page is less than the page we're trying to render.

  1. We allow lookupObject to cache Collections, and items, because I haven't written a DocumentLoader yet.


>>33985
Am pretty sure these constraints make the problem impossible…
Guess I'll deal with it later.

I'm still working on this algorithm. I'm trying my hand at formal specification.
The head of the algorithm is given as follows:

  • Pages are indexed as 1..N-1, Sentinel so that 1 is the oldest posts.
  • Page boundaries are completely stable.
  • We lazily load the item statuses, finishing if we've fetched the cached page or all the updates.
  • If there's no changes and we're fetching the end we skip to the end.


The Init and Next formula follow:

Init ==
  /\ TypeOK
  (* Insures "new" statuses are only in continuous ranges connected to the *)
  (* ends. *)
  /\ NewAtEndsOnly
  (* Set item and page to either jump to next or start at Sentinel *)
  /\ JumpToNext \/ GoToStart
  (* We do not assume a consistent pageSize for pages. *)
  (* We do not assume that pages are defragmented of a certain number *)
  /\ PageItemsMonotonicalIncreasing 
  /\ PagesLessThanPageSize
  (* statuses is a record of the state with respect to the pages cache. *)
  /\ NewItemsNotInPages
  /\ DeletedItemsInPages
  /\ UnmodifiedItemsInPages
  /\ changes = 0

Next ==
  \/ /\ statuses[item] = "new"
     (* If we've read all the changes needed we stop updating. *)
     /\ changes /= netChanges \/ ~Cached(desired)
     /\ pages' = [ pages EXCEPT ![page] = pages[page] \cup { item } ]
     /\ IF Cached(page)
        THEN changes' = changes + 1
        ELSE changes' = changes
     /\ Iterate
  \/ /\ statuses[item] = "deleted"
     /\ changes /= netChanges \/ ~Cached(desired)
     /\ pages' = [ pages EXCEPT ![page] = pages[page] \ { item } ]
     /\ IF Cached(page)
        THEN changes' = changes - 1
        ELSE changes' = changes
     /\ Iterate
  \/ /\ statuses[item] = "unmodified"
     /\ changes /= netChanges \/ ~Cached(desired)
     /\ pages' = pages
     /\ changes' = changes
     /\ Iterate

Think managed to get the math to check out.
Replaced the page variable with CHOOSE which picks the best location for the item.
And added a Init constraint that EmptyNewPages s.t. there are pages available for all the new items.
Had to replace most of the initial type declarations.
Did this to allow arbitrary subsets of Items, and because modulo for Sentinel size was no longer working.
Still not sure it's perfect.


Unique IPs: 4

[Return][Go to top] [Catalog] | [Home][Post a Reply]
Delete Post [ ]
[ home / rules / faq / search ] [ overboard / sfw / alt ] [ leftypol / edu / labor / siberia / lgbt / latam / hobby / tech / games / anime / music / draw / AKM / ufo / 420 ] [ meta ] [ wiki / shop / tv / tiktok / twitter / patreon ] [ GET / ref / marx / booru ]