module examples/assets/assets sig Catalog {} sig Asset {} one sig Undefined {} sig ApplicationState { catalogs: set Catalog, catalogState: catalogs -> one CatalogState, currentCatalog: catalogs, buffer: set Asset } sig CatalogState { assets: set Asset, part hidden, showing: set assets, selection: set assets + Undefined } pred appInv (xs: ApplicationState) { all cs: xs.catalogs | catalogInv (xs.catalogState[cs]) } pred catalogInv (cs: CatalogState) { cs.selection = Undefined or (some cs.selection and cs.selection in cs.showing) } pred showSelected (cs, cs': CatalogState) { cs.selection != Undefined cs'.showing = cs.selection cs'.selection = cs.selection cs'.assets = cs.assets } pred hideSelected (cs, cs': CatalogState) { cs.selection != Undefined cs'.hidden = cs.hidden + cs.selection cs'.selection = Undefined cs'.assets = cs.assets } pred cut (xs, xs': ApplicationState) { let cs = xs.currentCatalog.(xs.catalogState), sel = cs.selection { sel != Undefined xs'.buffer = sel some cs': CatalogState { cs'.assets = cs.assets - sel cs'.showing = cs.showing - sel cs'.selection = Undefined xs'.catalogState = xs.catalogState ++ xs.currentCatalog -> cs' } } xs'.catalogs = xs.catalogs xs'.currentCatalog = xs.currentCatalog } pred paste0 (xs, xs': ApplicationState) { xs'.catalogs = xs.catalogs xs'.currentCatalog = xs.currentCatalog let cs = xs.currentCatalog.(xs.catalogState), buf = xs.buffer { xs'.buffer = buf some cs': CatalogState { cs'.assets = cs.assets + buf cs'.showing = cs.showing + buf cs'.selection = buf xs'.catalogState = xs.catalogState ++ xs.currentCatalog -> cs' } } } pred paste1 (xs, xs': ApplicationState) { xs'.catalogs = xs.catalogs xs'.currentCatalog = xs.currentCatalog let cs = xs.currentCatalog.(xs.catalogState), buf = xs.buffer { xs'.buffer = buf some cs': CatalogState { cs'.assets = cs.assets + buf cs'.showing = cs.showing + buf cs'.selection = if some buf then buf else Undefined xs'.catalogState = xs.catalogState ++ xs.currentCatalog -> cs' } } } pred paste (xs, xs': ApplicationState) { xs'.catalogs = xs.catalogs xs'.currentCatalog = xs.currentCatalog let cs = xs.currentCatalog.(xs.catalogState), buf = xs.buffer { xs'.buffer = buf some cs': CatalogState { cs'.assets = cs.assets + buf cs'.showing = cs.showing + (buf - cs.assets) -- cs'.selection = buf - cs.assets cs'.selection = if some buf then buf - cs.assets else Undefined xs'.catalogState = xs.catalogState ++ xs.currentCatalog -> cs' } } } pred sameApplicationState (xs, xs': ApplicationState) { xs'.catalogs = xs.catalogs all c: xs.catalogs | sameCatalogState (c.(xs.catalogState), c.(xs'.catalogState)) xs'.currentCatalog = xs.currentCatalog -- xs'.buffer = xs.buffer } pred sameCatalogState (cs, cs': CatalogState) { cs'.assets = cs.assets cs'.showing = cs.showing -- cs'.selection = cs.selection } assert CutPaste { all xs, xs', xs": ApplicationState | (appInv (xs) and cut (xs, xs') and paste (xs', xs")) => sameApplicationState (xs, xs") } check CutPaste for 3 but 2 Asset assert PasteCut { all xs, xs', xs": ApplicationState | (appInv (xs) and paste (xs, xs') and cut (xs', xs")) => sameApplicationState (xs, xs") } check PasteCut for 3 but 2 Asset assert PasteNotAffectHidden { all xs, xs': ApplicationState | (appInv (xs) and paste (xs, xs')) => let c = xs.currentCatalog | xs'.catalogState[c].hidden = xs.catalogState[c].hidden } check PasteNotAffectHidden assert ShowPreservesInv { all cs, cs': CatalogState | catalogInv (cs) and showSelected (cs, cs') => catalogInv (cs') } check ShowPreservesInv assert PastePreservesInv { all xs, xs': ApplicationState | appInv (xs) and paste0 (xs, xs') => appInv (xs') } check PastePreservesInv for 3 but 2 ApplicationState, 2 CatalogState, 1 Asset assert HidePreservesInv { all cs, cs': CatalogState | catalogInv (cs) and hideSelected (cs, cs') => catalogInv (cs') } check HidePreservesInv /* pred copy (xs, xs': ApplicationState) { xs'.catalogs = xs.catalogs xs'.catalogState = xs.catalogState xs'.currentCatalog = xs.currentCatalog xs'.buffer = xs.currentCatalog.(xs.catalogState).selection } assert PasteCut' { all xs, xs', xs": ApplicationState | (appInv (xs) and paste (xs, xs') and cut (xs', xs") and no xs.buffer & xs.catalogState[xs.currentCatalog].assets) => sameApplicationState (xs, xs") } */