|
|
||||||
|
|
luafaudes Tutorial: op_fsmsynth_pc1_exit1_ics.luaTo run the below Lua script, cd to the tutorial section of the respective plug-in and enter luafaudes op_fsmsynth_pc1_exit1_ics.lua at the command prompt. The script will read input data from ./tutorial/data/. -- Perform the hierarchical synthesis for the Module "Distribution System" (DS) faudes.MakeGlobal() -- ================================= -- Basic Variables -- ================================= plantGen = System() specGen = Generator() spec1Gen = Generator() spec2Gen = Generator() spec3Gen = Generator() spec4Gen = Generator() spec5Gen = Generator() spec6Gen = Generator() spec7Gen = Generator() supGen = System() highGen = System() high1Gen = System() high2Gen = System() high3Gen = System() high5Gen = System() high6Gen = System() highAlph = EventSet() filePath = "data/fsmsynth/" supSize = 0 -- ============================================================================= -- ics, pc1 and exit1 (same supervisor computation for all types of abstractions -- ============================================================================= high1Gen= System("data/fsmsynth/pc1-exit1-ics/ics/ics[3]_msalcc.gen"); high2Gen= System("data/fsmsynth/pc1-exit1-ics/pc1/pc1[3]_msalcc.gen"); high3Gen= System("data/fsmsynth/pc1-exit1-ics/exit1/exit1[3]_msalcc.gen"); Parallel(high1Gen,high2Gen,supGen); Parallel(supGen,high3Gen,plantGen); plantGen:StateNamesEnabled(false); plantGen:Write("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[3].gen"); -- specification specGen = Generator("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[3]_spec.gen"); specGen:GraphWrite("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[3]_spec.png"); InvProject(specGen,plantGen:Alphabet() ); -- supervisor computation SupConNB(plantGen,specGen,supGen); supSize = supSize + supGen:Size() supGen:StateNamesEnabled(false); supGen:Write("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[3]_sup.gen"); -- ============ -- abstractions -- ============ -- msa-observer with LCC highAlph= EventSet("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[4]_orig.alph","Alphabet"); MsaObserverLcc(supGen,supGen:ControllableEvents(),highAlph); highAlph:Write("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[4]_msalcc.alph","Alphabet"); Project(supGen,highAlph,high1Gen); StateMin(high1Gen) print("State count of PC1-EXIT1-ICS abstraction: ", high1Gen:Size()) high1Gen:StateNamesEnabled(false); high1Gen:Write("data/fsmsynth/pc1-exit1-ics/pc1exit1ics[4]_msalcc.gen"); print("Accumulated state count of the PC1-EXIT1-ICS supervisors: ", supSize) -- record testcase FAUDES_TEST_DUMP("PC1EX1",supSize)
libFAUDES 2.32b --- 2024.03.01 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-luabindings-hybrid-example-pybindings" |