Mohan Radhakrishnan mohanr
mohanr
/ bayermoore.tla
Last active
December 19, 2022 11:19
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ----------------------------- MODULE bayermoore ----------------------------- | |
| EXTENDS Integers, Sequences,Naturals, TLC | |
| CONSTANTS Character, text, pattern | |
| ASSUME text \in Seq(Character) | |
| ASSUME pattern \in Seq(Character) | |
| Max(x,y) == IF x < y THEN y ELSE x | |
| struct == [a |-> 97, b |-> 98, c |-> 99] | |
| (*--algorithm bayermoore | |
| variables |
mohanr
/ bayermoore_translation.tla
Created
December 22, 2022 05:06
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \* BEGIN TRANSLATION (chksum(pcal) = "e913b13a" /\ chksum(tla) = "2d410eef") | |
| CONSTANT defaultInitValue | |
| VARIABLES i, m, l, n, j, k, p, skips, x, y, flag, pc | |
| vars == << i, m, l, n, j, k, p, skips, x, y, flag, pc >> | |
| Init == (* Global variables *) | |
| /\ i = defaultInitValue | |
| /\ m = defaultInitValue | |
| /\ l = defaultInitValue |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #lang typed/racket | |
| (require racket/list) | |
| (define (operator c ) | |
| (match c | |
| ['+' Plus] | |
| ['-' Minus] | |
| ['/' Div])) |
OlderNewer